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