Bob is blue. Bob is cold. Bob is nice. Bob is round. Gary is blue. Gary is quiet. Gary is round. Harry is blue. Harry is cold. Harry is kind. Harry is nice. Harry is red. Quiet people are round. If Gary is nice and Gary is cold then Gary is blue. All blue people are kind. Blue, quiet people are nice. All nice people are kind. All cold people are quiet.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If Gary is nice and Gary is cold then Gary is blue.
((("Gary" "is" "nice" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "blue" "+"))
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Blue, quiet people are nice.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
All nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
Harry is kind.
True
1
proof
[(triple10 OR ((triple11) -> rule5) OR ((triple8) -> rule3) OR ((((triple8 ((triple9) -> rule6)) -> rule4)) -> rule5))]
("Harry" "is" "kind" "+")
triple10
((triple11) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple8) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple8 ((triple9) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not kind.
False
1
inv-proof
[(triple10 OR ((triple11) -> rule5) OR ((triple8) -> rule3) OR ((((triple8 ((triple9) -> rule6)) -> rule4)) -> rule5))]
("Harry" "is" "kind" "-")
triple10
((triple11) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple8) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple8 ((triple9) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is quiet.
True
2
proof
[(((triple9) -> rule6))]
("Harry" "is" "quiet" "+")
((triple9) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple5) -> rule3) OR ((((triple5 triple6) -> rule4)) -> rule5))]
("Gary" "is" "kind" "-")
((triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple5 triple6) -> (rule4 % int2))) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Harry is round.
True
3
proof
[(((((triple9) -> rule6)) -> rule1))]
("Harry" "is" "round" "+")
((((triple9) -> (rule6 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple9) -> rule6)) -> rule1))]
("Harry" "is" "round" "-")
((((triple9) -> (rule6 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is nice.[(triple3 OR ((triple1 ((triple2) -> rule6)) -> rule4))] Bob is round.[(triple4 OR ((((triple2) -> rule6)) -> rule1))] Gary is blue.[(triple5)] Gary is quiet.[(triple6)] Gary is round.[(triple7 OR ((triple6) -> rule1))] Harry is blue.[(triple8)] Harry is cold.[(triple9)] Harry is kind.[(triple10 OR ((triple11) -> rule5) OR ((triple8) -> rule3) OR ((((triple8 ((triple9) -> rule6)) -> rule4)) -> rule5))] Harry is nice.[(triple11 OR ((triple8 ((triple9) -> rule6)) -> rule4))] Harry is red.[(triple12)] @1: Bob is kind.[(((triple1) -> rule3) OR ((triple3) -> rule5) OR ((((triple1 ((triple2) -> rule6)) -> rule4)) -> rule5))] Bob is quiet.[(((triple2) -> rule6))] Gary is kind.[(((triple5) -> rule3) OR ((((triple5 triple6) -> rule4)) -> rule5))] Gary is nice.[(((triple5 triple6) -> rule4))] Harry is quiet.[(((triple9) -> rule6))] @2: Harry is round.[(((((triple9) -> rule6)) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple1 ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple4
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
((triple6) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
((triple11) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple8) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple8 ((triple9) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple11
((triple8 ((triple9) -> (rule6 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple12
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple3) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple1 ((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple5 triple6) -> (rule4 % int2))) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((triple5 triple6) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple9) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple9) -> (rule6 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2