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