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