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