Dave is big. Dave is quiet. Dave is red. Dave is rough. Dave is round. Dave is white. Dave is young. Gary is big. Gary is rough. Gary is round. Gary is young. Harry is quiet. Harry is red. Harry is rough. Harry is round. Harry is young. Round people are red. If someone is round then they are red. If someone is quiet then they are round. If someone is big and white then they are round. If someone is big then they are white. All white people are quiet.
Dave is big.
("Dave" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
Round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is round then they are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is quiet then they are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If someone is big and white then they are round.
((("someone" "is" "big" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
All white people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
Harry is round.
True
1
proof
[(triple15 OR ((triple12) -> rule3))]
("Harry" "is" "round" "+")
triple15
((triple12) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
1
inv-proof
[(triple15 OR ((triple12) -> rule3))]
("Harry" "is" "round" "-")
triple15
((triple12) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Gary is red.
True
2
proof
[(((triple10) -> rule1) OR ((triple10) -> rule2) OR ((((triple8 ((triple8) -> rule5)) -> rule4)) -> rule1) OR ((((triple8 ((triple8) -> rule5)) -> rule4)) -> rule2) OR ((((((((triple8) -> rule5)) -> rule6)) -> rule3)) -> rule1) OR ((((((((triple8) -> rule5)) -> rule6)) -> rule3)) -> rule2))]
("Gary" "is" "red" "+")
((triple10) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple10) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple8 ((triple8) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((((triple8 ((triple8) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((((((((triple8) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
((((((((triple8) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is not white.
False
2
inv-proof
[(((triple8) -> rule5))]
("Gary" "is" "white" "-")
((triple8) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
True
3
proof
[(((((triple8) -> rule5)) -> rule6))]
("Gary" "is" "quiet" "+")
((((triple8) -> (rule5 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple8) -> rule5)) -> rule6))]
("Gary" "is" "quiet" "-")
((((triple8) -> (rule5 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Dave is big.[(triple1)] Dave is quiet.[(triple2 OR ((triple6) -> rule6) OR ((((triple1) -> rule5)) -> rule6))] Dave is red.[(triple3 OR ((triple5) -> rule1) OR ((triple5) -> rule2) OR ((((triple2) -> rule3)) -> rule1) OR ((((triple2) -> rule3)) -> rule2) OR ((((triple1 triple6) -> rule4)) -> rule1) OR ((((triple1 triple6) -> rule4)) -> rule2) OR ((((((triple6) -> rule6)) -> rule3)) -> rule1) OR ((((((triple6) -> rule6)) -> rule3)) -> rule2) OR ((((triple1 ((triple1) -> rule5)) -> rule4)) -> rule1) OR ((((triple1 ((triple1) -> rule5)) -> rule4)) -> rule2) OR ((((((((triple1) -> rule5)) -> rule6)) -> rule3)) -> rule1) OR ((((((((triple1) -> rule5)) -> rule6)) -> rule3)) -> rule2))] Dave is rough.[(triple4)] Dave is round.[(triple5 OR ((triple2) -> rule3) OR ((triple1 triple6) -> rule4) OR ((((triple6) -> rule6)) -> rule3) OR ((triple1 ((triple1) -> rule5)) -> rule4) OR ((((((triple1) -> rule5)) -> rule6)) -> rule3))] Dave is white.[(triple6 OR ((triple1) -> rule5))] Dave is young.[(triple7)] Gary is big.[(triple8)] Gary is rough.[(triple9)] Gary is round.[(triple10 OR ((triple8 ((triple8) -> rule5)) -> rule4) OR ((((((triple8) -> rule5)) -> rule6)) -> rule3))] Gary is young.[(triple11)] Harry is quiet.[(triple12)] Harry is red.[(triple13 OR ((triple15) -> rule1) OR ((triple15) -> rule2) OR ((((triple12) -> rule3)) -> rule1) OR ((((triple12) -> rule3)) -> rule2))] Harry is rough.[(triple14)] Harry is round.[(triple15 OR ((triple12) -> rule3))] Harry is young.[(triple16)] @1: Gary is red.[(((triple10) -> rule1) OR ((triple10) -> rule2) OR ((((triple8 ((triple8) -> rule5)) -> rule4)) -> rule1) OR ((((triple8 ((triple8) -> rule5)) -> rule4)) -> rule2) OR ((((((((triple8) -> rule5)) -> rule6)) -> rule3)) -> rule1) OR ((((((((triple8) -> rule5)) -> rule6)) -> rule3)) -> rule2))] Gary is white.[(((triple8) -> rule5))] @2: Gary is quiet.[(((((triple8) -> rule5)) -> rule6))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
((triple6) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple3
((triple5) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple5) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple1 triple6) -> (rule4 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple1 triple6) -> (rule4 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((((triple6) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((((triple1) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((((((triple1) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
((triple2) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple1 triple6) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((triple1 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple1) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple10
((triple8 ((triple8) -> (rule5 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((((triple8) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
((triple15) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple15) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
((triple12) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple16
Gary is red.
("Gary" "is" "red" "+")
((triple10) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple10) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple8 ((triple8) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((((triple8 ((triple8) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((((((((triple8) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
((((((((triple8) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
((triple8) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple8) -> (rule5 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2