Bob is nice. Bob is white. Dave is cold. Dave is white. Gary is nice. Gary is quiet. Harry is big. If something is quiet and big then it is red. White, cold things are red. Big things are quiet. All red things are quiet. If Harry is red and Harry is big then Harry is nice. If something is white and nice then it is blue. If Gary is big and Gary is cold then Gary is white. If Harry is blue and Harry is nice then Harry is quiet.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is big.
("Harry" "is" "big" "+")
If something is quiet and big then it is red.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
White, cold things are red.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If Harry is red and Harry is big then Harry is nice.
((("Harry" "is" "red" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "nice" "+"))
If something is white and nice then it is blue.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If Gary is big and Gary is cold then Gary is white.
((("Gary" "is" "big" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "white" "+"))
If Harry is blue and Harry is nice then Harry is quiet.
((("Harry" "is" "blue" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "quiet" "+"))
Harry is big.
True
1
proof
[(triple7)]
("Harry" "is" "big" "+")
triple7
Bob is not white.
False
1
inv-proof
[(triple2)]
("Bob" "is" "white" "-")
triple2
Dave is red.
True
3
proof
[(((triple4 triple3) -> rule2))]
("Dave" "is" "red" "+")
((triple4 triple3) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
3
inv-proof
[(((triple4 triple3) -> rule2))]
("Dave" "is" "red" "-")
((triple4 triple3) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
True
4
proof
[(((((triple4 triple3) -> rule2)) -> rule4))]
("Dave" "is" "quiet" "+")
((((triple4 triple3) -> (rule2 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Harry is not red.
False
4
inv-proof
[(((((triple7) -> rule3) triple7) -> rule1))]
("Harry" "is" "red" "-")
((((triple7) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
True
6
proof
[(((((((triple7) -> rule3) triple7) -> rule1) triple7) -> rule5))]
("Harry" "is" "nice" "+")
((((((triple7) -> (rule3 % int3)) triple7) -> (rule1 % int2)) triple7) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not nice.
False
6
inv-proof
[(((((((triple7) -> rule3) triple7) -> rule1) triple7) -> rule5))]
("Harry" "is" "nice" "-")
((((((triple7) -> (rule3 % int3)) triple7) -> (rule1 % int2)) triple7) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "blue" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "red" "+")
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is blue.
Unknown
rconc
[@2: Gary is blue.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Gary" "is" "blue" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is nice.[(triple1)] Bob is white.[(triple2)] Dave is cold.[(triple3)] Dave is white.[(triple4)] Gary is nice.[(triple5)] Gary is quiet.[(triple6)] Harry is big.[(triple7)] @1: Bob is blue.[(((triple2 triple1) -> rule6))] Dave is red.[(((triple4 triple3) -> rule2))] Harry is quiet.[(((triple7) -> rule3))] @2: Dave is quiet.[(((((triple4 triple3) -> rule2)) -> rule4))] Harry is red.[(((((triple7) -> rule3) triple7) -> rule1))] @3: Harry is nice.[(((((((triple7) -> rule3) triple7) -> rule1) triple7) -> rule5))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Bob is blue.
("Bob" "is" "blue" "+")
((triple2 triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple4 triple3) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple7) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple4 triple3) -> (rule2 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple7) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple7) -> (rule3 % int3)) triple7) -> (rule1 % int2)) triple7) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3