Bob is nice. Charlie is round. Charlie is smart. Gary is blue. Gary is not nice. Gary is not smart. Harry is nice. All smart things are blue. If something is nice then it is blue. All round things are blue. If Bob is red then Bob is rough. Big, blue things are red. Blue things are red. Rough things are round. If something is round and not smart then it is rough. Round, red things are big.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not nice.
("Gary" "is" "nice" "-")
Gary is not smart.
("Gary" "is" "smart" "-")
Harry is nice.
("Harry" "is" "nice" "+")
All smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If something is nice then it is blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
All round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If Bob is red then Bob is rough.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "rough" "+"))
Big, blue things are red.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is round and not smart then it is rough.
((("something" "is" "round" "+") ("something" "is" "smart" "~")) -> ("something" "is" "rough" "+"))
Round, red things are big.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Gary is not smart.
True
1
proof
[(triple6)]
("Gary" "is" "smart" "-")
triple6
Gary is not blue.
False
1
inv-proof
[(triple4)]
("Gary" "is" "blue" "-")
triple4
Harry is blue.
True
2
proof
[(((triple7) -> rule2))]
("Harry" "is" "blue" "+")
((triple7) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "blue" "-")
((triple1) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Charlie is red.
True
3
proof
[(((((triple2) -> rule3)) -> rule6) OR ((((triple3) -> rule1)) -> rule6))]
("Charlie" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Harry is not red.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule6))]
("Harry" "is" "red" "-")
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Bob is rough.
True
4
proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule4))]
("Bob" "is" "rough" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Charlie is not big.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule3)) -> rule6)) -> rule9) OR ((triple2 ((((triple3) -> rule1)) -> rule6)) -> rule9))]
("Charlie" "is" "big" "-")
((triple2 ((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((triple2 ((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Bob is round.
True
5
proof
[(((((((((triple1) -> rule2)) -> rule6)) -> rule4)) -> rule7))]
("Bob" "is" "round" "+")
((((((((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is not round.
False
5
inv-proof
[(((((((((triple1) -> rule2)) -> rule6)) -> rule4)) -> rule7))]
("Bob" "is" "round" "-")
((((((((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is big.
True
9
proof
[(((((((((((triple1) -> rule2)) -> rule6)) -> rule4)) -> rule7) ((((triple1) -> rule2)) -> rule6)) -> rule9))]
("Bob" "is" "big" "+")
((((((((((triple1) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule7 % int2)) ((((triple1) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule9 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is blue.
("Bob" "is" "blue" "+")
int5
Bob is not big.
False
9
inv-proof
[(((((((((((triple1) -> rule2)) -> rule6)) -> rule4)) -> rule7) ((((triple1) -> rule2)) -> rule6)) -> rule9))]
("Bob" "is" "big" "-")
((((((((((triple1) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule7 % int2)) ((((triple1) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule9 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is blue.
("Bob" "is" "blue" "+")
int5
Harry is not big.
Unknown
inv-rconc
[@3: Harry is big.[CWA. Example of deepest failure = (rule9 <- rule7 <- rule8 <- FAIL)]]
("Harry" "is" "big" "-")
Harry is round.
Unknown
rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("Harry" "is" "round" "+")
Gary is not round.
Unknown
inv-rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is rough.
Unknown
rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "rough" "+")
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "rough" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "rough" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Bob is nice.[(triple1)] Charlie is round.[(triple2)] Charlie is smart.[(triple3)] Gary is blue.[(triple4)] Gary is not nice.[(triple5)] Gary is not smart.[(triple6)] Harry is nice.[(triple7)] @1: Bob is blue.[(((triple1) -> rule2))] Charlie is blue.[(((triple2) -> rule3) OR ((triple3) -> rule1))] Gary is red.[(((triple4) -> rule6))] Harry is blue.[(((triple7) -> rule2))] @2: Bob is red.[(((((triple1) -> rule2)) -> rule6))] Charlie is red.[(((((triple2) -> rule3)) -> rule6) OR ((((triple3) -> rule1)) -> rule6))] Harry is red.[(((((triple7) -> rule2)) -> rule6))] @3: Bob is rough.[(((((((triple1) -> rule2)) -> rule6)) -> rule4))] Charlie is big.[(((triple2 ((((triple2) -> rule3)) -> rule6)) -> rule9) OR ((triple2 ((((triple3) -> rule1)) -> rule6)) -> rule9))] @4: Bob is round.[(((((((((triple1) -> rule2)) -> rule6)) -> rule4)) -> rule7))] @5: Bob is big.[(((((((((((triple1) -> rule2)) -> rule6)) -> rule4)) -> rule7) ((((triple1) -> rule2)) -> rule6)) -> rule9))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Gary is not nice.
("Gary" "is" "nice" "-")
triple5
Gary is not smart.
("Gary" "is" "smart" "-")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple3) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple4) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple7) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
((triple2 ((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((triple2 ((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
((((((((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is big.
("Bob" "is" "big" "+")
((((((((((triple1) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule7 % int2)) ((((triple1) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule9 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is blue.
("Bob" "is" "blue" "+")
int5