Anne is big. Anne is cold. Anne is nice. Anne is quiet. Anne is rough. Anne is white. Charlie is not cold. Fiona is cold. Fiona is white. Gary is big. Gary is blue. Blue things are big. If Fiona is blue and Fiona is white then Fiona is not big. If Fiona is big then Fiona is quiet. If something is white then it is cold. Blue, nice things are cold. Blue things are rough. All cold, white things are nice. All quiet things are white. Rough, blue things are quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If Fiona is blue and Fiona is white then Fiona is not big.
((("Fiona" "is" "blue" "+") ("Fiona" "is" "white" "+")) -> ("Fiona" "is" "big" "-"))
If Fiona is big then Fiona is quiet.
((("Fiona" "is" "big" "+")) -> ("Fiona" "is" "quiet" "+"))
If something is white then it is cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Blue, nice things are cold.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
All cold, white things are nice.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
All quiet things are white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Rough, blue things are quiet.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Anne is rough.
True
1
proof
[(triple5)]
("Anne" "is" "rough" "+")
triple5
Anne is not white.
False
1
inv-proof
[(triple6 OR ((triple4) -> rule8))]
("Anne" "is" "white" "-")
triple6
((triple4) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Fiona is nice.
True
3
proof
[(((triple8 triple9) -> rule7) OR ((((triple9) -> rule4) triple9) -> rule7))]
("Fiona" "is" "nice" "+")
((triple8 triple9) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple9) -> (rule4 % int2)) triple9) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Gary is not rough.
False
2
inv-proof
[(((triple11) -> rule6))]
("Gary" "is" "rough" "-")
((triple11) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
True
4
proof
[(((((triple11) -> rule6) triple11) -> rule9))]
("Gary" "is" "quiet" "+")
((((triple11) -> (rule6 % int2)) triple11) -> (rule9 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not quiet.
False
4
inv-proof
[(((((triple11) -> rule6) triple11) -> rule9))]
("Gary" "is" "quiet" "-")
((((triple11) -> (rule6 % int2)) triple11) -> (rule9 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is white.
True
5
proof
[(((((((triple11) -> rule6) triple11) -> rule9)) -> rule8))]
("Gary" "is" "white" "+")
((((((triple11) -> (rule6 % int3)) triple11) -> (rule9 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is not white.
False
5
inv-proof
[(((((((triple11) -> rule6) triple11) -> rule9)) -> rule8))]
("Gary" "is" "white" "-")
((((((triple11) -> (rule6 % int3)) triple11) -> (rule9 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is cold.
True
6
proof
[(((((((((triple11) -> rule6) triple11) -> rule9)) -> rule8)) -> rule4))]
("Gary" "is" "cold" "+")
((((((((triple11) -> (rule6 % int4)) triple11) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is not cold.
False
6
inv-proof
[(((((((((triple11) -> rule6) triple11) -> rule9)) -> rule8)) -> rule4))]
("Gary" "is" "cold" "-")
((((((((triple11) -> (rule6 % int4)) triple11) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is nice.
True
12
proof
[(((((((((((triple11) -> rule6) triple11) -> rule9)) -> rule8)) -> rule4) ((((((triple11) -> rule6) triple11) -> rule9)) -> rule8)) -> rule7))]
("Gary" "is" "nice" "+")
((((((((((triple11) -> (rule6 % int5)) triple11) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) ((((((triple11) -> (rule6 % int5)) triple11) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5
Gary is not nice.
False
12
inv-proof
[(((((((((((triple11) -> rule6) triple11) -> rule9)) -> rule8)) -> rule4) ((((((triple11) -> rule6) triple11) -> rule9)) -> rule8)) -> rule7))]
("Gary" "is" "nice" "-")
((((((((((triple11) -> (rule6 % int5)) triple11) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) ((((((triple11) -> (rule6 % int5)) triple11) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is white.
Unknown
rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule8 <- rule9 <- FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "big" "+")
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "big" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2 OR ((triple6) -> rule4) OR ((((triple4) -> rule8)) -> rule4))] Anne is nice.[(triple3 OR ((triple2 triple6) -> rule7) OR ((triple2 ((triple4) -> rule8)) -> rule7) OR ((((triple6) -> rule4) triple6) -> rule7) OR ((((triple6) -> rule4) ((triple4) -> rule8)) -> rule7) OR ((((((triple4) -> rule8)) -> rule4) triple6) -> rule7) OR ((((((triple4) -> rule8)) -> rule4) ((triple4) -> rule8)) -> rule7))] Anne is quiet.[(triple4)] Anne is rough.[(triple5)] Anne is white.[(triple6 OR ((triple4) -> rule8))] Charlie is not cold.[(triple7)] Fiona is cold.[(triple8 OR ((triple9) -> rule4))] Fiona is white.[(triple9)] Gary is big.[(triple10 OR ((triple11) -> rule1))] Gary is blue.[(triple11)] @1: Fiona is nice.[(((triple8 triple9) -> rule7) OR ((((triple9) -> rule4) triple9) -> rule7))] Gary is rough.[(((triple11) -> rule6))] @2: Gary is quiet.[(((((triple11) -> rule6) triple11) -> rule9))] @3: Gary is white.[(((((((triple11) -> rule6) triple11) -> rule9)) -> rule8))] @4: Gary is cold.[(((((((((triple11) -> rule6) triple11) -> rule9)) -> rule8)) -> rule4))] @5: Gary is nice.[(((((((((((triple11) -> rule6) triple11) -> rule9)) -> rule8)) -> rule4) ((((((triple11) -> rule6) triple11) -> rule9)) -> rule8)) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple6) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple4) -> (rule8 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((triple2 triple6) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((triple2 ((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple6) -> (rule4 % int2)) triple6) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple6) -> (rule4 % int3)) ((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((triple4) -> (rule8 % int3))) -> (rule4 % int2)) triple6) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((((triple4) -> (rule8 % int3))) -> (rule4 % int2)) ((triple4) -> (rule8 % int3))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple4) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple7
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
((triple9) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple9
Gary is big.
("Gary" "is" "big" "+")
triple10
((triple11) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple11
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple8 triple9) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple9) -> (rule4 % int2)) triple9) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple11) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple11) -> (rule6 % int2)) triple11) -> (rule9 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((((triple11) -> (rule6 % int3)) triple11) -> (rule9 % int2))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
((((((((triple11) -> (rule6 % int4)) triple11) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is nice.
("Gary" "is" "nice" "+")
((((((((((triple11) -> (rule6 % int5)) triple11) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) ((((((triple11) -> (rule6 % int5)) triple11) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5