Bob is rough. Bob is young. Charlie is round. Charlie is young. Erin is blue. Erin is cold. Erin is rough. Erin is round. Fiona is blue. Fiona is cold. Rough, round things are young. Cold things are round. If something is round and cold then it is quiet. Rough, blue things are round. If Fiona is round and Fiona is rough then Fiona is cold. If something is blue then it is rough.
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Rough, round things are young.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
Cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is round and cold then it is quiet.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Rough, blue things are round.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If Fiona is round and Fiona is rough then Fiona is cold.
((("Fiona" "is" "round" "+") ("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "cold" "+"))
If something is blue then it is rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Fiona is cold.
True
1
proof
[(triple10 OR ((((((triple9) -> rule6) triple9) -> rule4) ((triple9) -> rule6)) -> rule5))]
("Fiona" "is" "cold" "+")
triple10
((((((triple9) -> (rule6 % int3)) triple9) -> (rule4 % int2)) ((triple9) -> (rule6 % int3))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Erin is not round.
False
1
inv-proof
[(triple8 OR ((triple6) -> rule2) OR ((triple7 triple5) -> rule4) OR ((((triple5) -> rule6) triple5) -> rule4))]
("Erin" "is" "round" "-")
triple8
((triple6) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple7 triple5) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple5) -> (rule6 % int2)) triple5) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Fiona is round.
True
2
proof
[(((triple10) -> rule2) OR ((((triple9) -> rule6) triple9) -> rule4))]
("Fiona" "is" "round" "+")
((triple10) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple9) -> (rule6 % int2)) triple9) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Erin is not young.
False
3
inv-proof
[(((triple7 triple8) -> rule1) OR ((triple7 ((triple6) -> rule2)) -> rule1) OR ((triple7 ((triple7 triple5) -> rule4)) -> rule1) OR ((((triple5) -> rule6) triple8) -> rule1) OR ((((triple5) -> rule6) ((triple6) -> rule2)) -> rule1) OR ((((triple5) -> rule6) ((triple7 triple5) -> rule4)) -> rule1) OR ((triple7 ((((triple5) -> rule6) triple5) -> rule4)) -> rule1) OR ((((triple5) -> rule6) ((((triple5) -> rule6) triple5) -> rule4)) -> rule1))]
("Erin" "is" "young" "-")
((triple7 triple8) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple7 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((triple7 ((triple7 triple5) -> (rule4 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple5) -> (rule6 % int2)) triple8) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple5) -> (rule6 % int3)) ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((triple5) -> (rule6 % int3)) ((triple7 triple5) -> (rule4 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((triple7 ((((triple5) -> (rule6 % int3)) triple5) -> (rule4 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((triple5) -> (rule6 % int3)) ((((triple5) -> (rule6 % int3)) triple5) -> (rule4 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Fiona is quiet.
True
4
proof
[(((((triple10) -> rule2) triple10) -> rule3) OR ((((((triple9) -> rule6) triple9) -> rule4) triple10) -> rule3) OR ((((triple10) -> rule2) ((((((triple9) -> rule6) triple9) -> rule4) ((triple9) -> rule6)) -> rule5)) -> rule3) OR ((((((triple9) -> rule6) triple9) -> rule4) ((((((triple9) -> rule6) triple9) -> rule4) ((triple9) -> rule6)) -> rule5)) -> rule3))]
("Fiona" "is" "quiet" "+")
((((triple10) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((((triple9) -> (rule6 % int3)) triple9) -> (rule4 % int2)) triple10) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((triple10) -> (rule2 % int4)) ((((((triple9) -> (rule6 % int3)) triple9) -> (rule4 % int4)) ((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
((((((triple9) -> (rule6 % int4)) triple9) -> (rule4 % int3)) ((((((triple9) -> (rule6 % int4)) triple9) -> (rule4 % int3)) ((triple9) -> (rule6 % int4))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is not quiet.
False
4
inv-proof
[(((((triple10) -> rule2) triple10) -> rule3) OR ((((((triple9) -> rule6) triple9) -> rule4) triple10) -> rule3) OR ((((triple10) -> rule2) ((((((triple9) -> rule6) triple9) -> rule4) ((triple9) -> rule6)) -> rule5)) -> rule3) OR ((((((triple9) -> rule6) triple9) -> rule4) ((((((triple9) -> rule6) triple9) -> rule4) ((triple9) -> rule6)) -> rule5)) -> rule3))]
("Fiona" "is" "quiet" "-")
((((triple10) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((((triple9) -> (rule6 % int3)) triple9) -> (rule4 % int2)) triple10) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((triple10) -> (rule2 % int4)) ((((((triple9) -> (rule6 % int3)) triple9) -> (rule4 % int4)) ((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
((((((triple9) -> (rule6 % int4)) triple9) -> (rule4 % int3)) ((((((triple9) -> (rule6 % int4)) triple9) -> (rule4 % int3)) ((triple9) -> (rule6 % int4))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "round" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Bob is rough.[(triple1)] Bob is young.[(triple2)] Charlie is round.[(triple3)] Charlie is young.[(triple4)] Erin is blue.[(triple5)] Erin is cold.[(triple6)] Erin is rough.[(triple7 OR ((triple5) -> rule6))] Erin is round.[(triple8 OR ((triple6) -> rule2) OR ((triple7 triple5) -> rule4) OR ((((triple5) -> rule6) triple5) -> rule4))] Fiona is blue.[(triple9)] Fiona is cold.[(triple10 OR ((((((triple9) -> rule6) triple9) -> rule4) ((triple9) -> rule6)) -> rule5))] @1: Erin is quiet.[(((triple8 triple6) -> rule3) OR ((((triple6) -> rule2) triple6) -> rule3) OR ((((triple7 triple5) -> rule4) triple6) -> rule3) OR ((((((triple5) -> rule6) triple5) -> rule4) triple6) -> rule3))] Erin is young.[(((triple7 triple8) -> rule1) OR ((triple7 ((triple6) -> rule2)) -> rule1) OR ((triple7 ((triple7 triple5) -> rule4)) -> rule1) OR ((((triple5) -> rule6) triple8) -> rule1) OR ((((triple5) -> rule6) ((triple6) -> rule2)) -> rule1) OR ((((triple5) -> rule6) ((triple7 triple5) -> rule4)) -> rule1) OR ((triple7 ((((triple5) -> rule6) triple5) -> rule4)) -> rule1) OR ((((triple5) -> rule6) ((((triple5) -> rule6) triple5) -> rule4)) -> rule1))] Fiona is rough.[(((triple9) -> rule6))] Fiona is round.[(((triple10) -> rule2) OR ((((triple9) -> rule6) triple9) -> rule4))] @2: Fiona is quiet.[(((((triple10) -> rule2) triple10) -> rule3) OR ((((((triple9) -> rule6) triple9) -> rule4) triple10) -> rule3) OR ((((triple10) -> rule2) ((((((triple9) -> rule6) triple9) -> rule4) ((triple9) -> rule6)) -> rule5)) -> rule3) OR ((((((triple9) -> rule6) triple9) -> rule4) ((((((triple9) -> rule6) triple9) -> rule4) ((triple9) -> rule6)) -> rule5)) -> rule3))] Fiona is young.[(((((triple9) -> rule6) ((triple10) -> rule2)) -> rule1) OR ((((triple9) -> rule6) ((((triple9) -> rule6) triple9) -> rule4)) -> rule1))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
((triple5) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple8
((triple6) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple7 triple5) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple5) -> (rule6 % int2)) triple5) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
Fiona is cold.
("Fiona" "is" "cold" "+")
triple10
((((((triple9) -> (rule6 % int3)) triple9) -> (rule4 % int2)) ((triple9) -> (rule6 % int3))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple8 triple6) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple6) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple7 triple5) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((((triple5) -> (rule6 % int3)) triple5) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
((triple7 triple8) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple7 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((triple7 ((triple7 triple5) -> (rule4 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple5) -> (rule6 % int2)) triple8) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple5) -> (rule6 % int3)) ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((triple5) -> (rule6 % int3)) ((triple7 triple5) -> (rule4 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((triple7 ((((triple5) -> (rule6 % int3)) triple5) -> (rule4 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((triple5) -> (rule6 % int3)) ((((triple5) -> (rule6 % int3)) triple5) -> (rule4 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple9) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple10) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple9) -> (rule6 % int2)) triple9) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple10) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((((triple9) -> (rule6 % int3)) triple9) -> (rule4 % int2)) triple10) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((triple10) -> (rule2 % int4)) ((((((triple9) -> (rule6 % int3)) triple9) -> (rule4 % int4)) ((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
((((((triple9) -> (rule6 % int4)) triple9) -> (rule4 % int3)) ((((((triple9) -> (rule6 % int4)) triple9) -> (rule4 % int3)) ((triple9) -> (rule6 % int4))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is young.
("Fiona" "is" "young" "+")
((((triple9) -> (rule6 % int3)) ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((((triple9) -> (rule6 % int3)) ((((triple9) -> (rule6 % int3)) triple9) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3