Anne is quiet. Anne is round. Anne is white. Anne is young. Charlie is big. Charlie is blue. Charlie is quiet. Charlie is white. Charlie is young. Erin is big. Erin is blue. Erin is quiet. Erin is rough. Erin is round. Erin is white. Erin is young. Blue, round things are rough. If something is blue then it is quiet. If something is big then it is white. Rough, round things are quiet. All white things are young. Big things are rough.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Blue, round things are rough.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something is blue then it is quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is big then it is white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
Rough, round things are quiet.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
All white things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
Big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Charlie is white.
True
1
proof
[(triple8 OR ((triple5) -> rule3))]
("Charlie" "is" "white" "+")
triple8
((triple5) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Erin is not round.
False
1
inv-proof
[(triple14)]
("Erin" "is" "round" "-")
triple14
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is quiet.[(triple1)] Anne is round.[(triple2)] Anne is white.[(triple3)] Anne is young.[(triple4 OR ((triple3) -> rule5))] Charlie is big.[(triple5)] Charlie is blue.[(triple6)] Charlie is quiet.[(triple7 OR ((triple6) -> rule2))] Charlie is white.[(triple8 OR ((triple5) -> rule3))] Charlie is young.[(triple9 OR ((triple8) -> rule5) OR ((((triple5) -> rule3)) -> rule5))] Erin is big.[(triple10)] Erin is blue.[(triple11)] Erin is quiet.[(triple12 OR ((triple11) -> rule2) OR ((triple13 triple14) -> rule4) OR ((((triple10) -> rule6) triple14) -> rule4) OR ((((triple11 triple14) -> rule1) triple14) -> rule4))] Erin is rough.[(triple13 OR ((triple10) -> rule6) OR ((triple11 triple14) -> rule1))] Erin is round.[(triple14)] Erin is white.[(triple15 OR ((triple10) -> rule3))] Erin is young.[(triple16 OR ((triple15) -> rule5) OR ((((triple10) -> rule3)) -> rule5))] @1: Charlie is rough.[(((triple5) -> rule6))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
((triple3) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple7
((triple6) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple8
((triple5) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple9
((triple8) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
triple10
Erin is blue.
("Erin" "is" "blue" "+")
triple11
Erin is quiet.
("Erin" "is" "quiet" "+")
triple12
((triple11) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple13 triple14) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple10) -> (rule6 % int2)) triple14) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple11 triple14) -> (rule1 % int2)) triple14) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple13
((triple10) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple11 triple14) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple14
Erin is white.
("Erin" "is" "white" "+")
triple15
((triple10) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple16
((triple15) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple5) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1