Bob is big. Bob is blue. Bob is green. Bob is quiet. Bob is rough. Bob is round. Charlie is green. Charlie is quiet. Charlie is rough. Charlie is round. Fiona is big. Fiona is blue. Fiona is green. Fiona is rough. Fiona is round. Fiona is white. Big people are white. If Bob is green then Bob is round. All round, quiet people are white. Quiet people are white. If someone is big then they are green. If Bob is green and Bob is round then Bob is rough. Big people are blue. Quiet people are white.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If Bob is green then Bob is round.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "round" "+"))
All round, quiet people are white.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is big then they are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If Bob is green and Bob is round then Bob is rough.
((("Bob" "is" "green" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "rough" "+"))
Big people are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
Quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Bob is round.
True
1
proof
[(triple6 OR ((triple3) -> rule2) OR ((((triple1) -> rule5)) -> rule2))]
("Bob" "is" "round" "+")
triple6
((triple3) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Fiona is not blue.
False
1
inv-proof
[(triple12 OR ((triple11) -> rule7))]
("Fiona" "is" "blue" "-")
triple12
((triple11) -> (rule7 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Bob is white.
True
2
proof
[(((triple1) -> rule1) OR ((triple4) -> rule4) OR ((triple4) -> rule8) OR ((triple6 triple4) -> rule3) OR ((((triple3) -> rule2) triple4) -> rule3) OR ((((((triple1) -> rule5)) -> rule2) triple4) -> rule3))]
("Bob" "is" "white" "+")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple4) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple4) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple6 triple4) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple3) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Charlie is not white.
False
2
inv-proof
[(((triple8) -> rule4) OR ((triple8) -> rule8) OR ((triple10 triple8) -> rule3))]
("Charlie" "is" "white" "-")
((triple8) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple8) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple10 triple8) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2 OR ((triple1) -> rule7))] Bob is green.[(triple3 OR ((triple1) -> rule5))] Bob is quiet.[(triple4)] Bob is rough.[(triple5 OR ((triple3 triple6) -> rule6) OR ((triple3 ((triple3) -> rule2)) -> rule6) OR ((((triple1) -> rule5) triple6) -> rule6) OR ((((triple1) -> rule5) ((triple3) -> rule2)) -> rule6) OR ((triple3 ((((triple1) -> rule5)) -> rule2)) -> rule6) OR ((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule2)) -> rule6))] Bob is round.[(triple6 OR ((triple3) -> rule2) OR ((((triple1) -> rule5)) -> rule2))] Charlie is green.[(triple7)] Charlie is quiet.[(triple8)] Charlie is rough.[(triple9)] Charlie is round.[(triple10)] Fiona is big.[(triple11)] Fiona is blue.[(triple12 OR ((triple11) -> rule7))] Fiona is green.[(triple13 OR ((triple11) -> rule5))] Fiona is rough.[(triple14)] Fiona is round.[(triple15)] Fiona is white.[(triple16 OR ((triple11) -> rule1))] @1: Bob is white.[(((triple1) -> rule1) OR ((triple4) -> rule4) OR ((triple4) -> rule8) OR ((triple6 triple4) -> rule3) OR ((((triple3) -> rule2) triple4) -> rule3) OR ((((((triple1) -> rule5)) -> rule2) triple4) -> rule3))] Charlie is white.[(((triple8) -> rule4) OR ((triple8) -> rule8) OR ((triple10 triple8) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple1) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple3
((triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple3 triple6) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple3 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple1) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple1) -> (rule5 % int3)) ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((triple3 ((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple3) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple8
Charlie is rough.
("Charlie" "is" "rough" "+")
triple9
Charlie is round.
("Charlie" "is" "round" "+")
triple10
Fiona is big.
("Fiona" "is" "big" "+")
triple11
Fiona is blue.
("Fiona" "is" "blue" "+")
triple12
((triple11) -> (rule7 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple13
((triple11) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple14
Fiona is round.
("Fiona" "is" "round" "+")
triple15
Fiona is white.
("Fiona" "is" "white" "+")
triple16
((triple11) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple4) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple4) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple6 triple4) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple3) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
((triple8) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple8) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple10 triple8) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1