Bob is blue. Bob is cold. Bob is furry. Bob is quiet. Bob is white. Charlie is blue. Charlie is cold. Charlie is furry. Charlie is kind. Charlie is nice. Charlie is quiet. Charlie is white. Harry is furry. Harry is nice. Harry is quiet. If something is nice and blue then it is kind. If something is furry and blue then it is cold. White things are kind. If something is cold then it is white. All cold, quiet things are furry. If something is nice and furry then it is cold.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is nice and blue then it is kind.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is furry and blue then it is cold.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
White things are kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
If something is cold then it is white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
All cold, quiet things are furry.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If something is nice and furry then it is cold.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Harry is quiet.
True
1
proof
[(triple15)]
("Harry" "is" "quiet" "+")
triple15
Charlie is not blue.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "blue" "-")
triple6
Bob is kind.
True
2
proof
[(((triple5) -> rule3) OR ((((triple2) -> rule4)) -> rule3) OR ((((((triple3 triple1) -> rule2)) -> rule4)) -> rule3))]
("Bob" "is" "kind" "+")
((triple5) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((((triple3 triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Harry is not cold.
False
3
inv-proof
[(((triple14 triple13) -> rule6))]
("Harry" "is" "cold" "-")
((triple14 triple13) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
True
4
proof
[(((((triple14 triple13) -> rule6)) -> rule4))]
("Harry" "is" "white" "+")
((((triple14 triple13) -> (rule6 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not white.
False
4
inv-proof
[(((((triple14 triple13) -> rule6)) -> rule4))]
("Harry" "is" "white" "-")
((((triple14 triple13) -> (rule6 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is kind.
True
5
proof
[(((((((triple14 triple13) -> rule6)) -> rule4)) -> rule3))]
("Harry" "is" "kind" "+")
((((((triple14 triple13) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not kind.
False
5
inv-proof
[(((((((triple14 triple13) -> rule6)) -> rule4)) -> rule3))]
("Harry" "is" "kind" "-")
((((((triple14 triple13) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2 OR ((triple3 triple1) -> rule2))] Bob is furry.[(triple3 OR ((triple2 triple4) -> rule5))] Bob is quiet.[(triple4)] Bob is white.[(triple5 OR ((triple2) -> rule4) OR ((((triple3 triple1) -> rule2)) -> rule4))] Charlie is blue.[(triple6)] Charlie is cold.[(triple7 OR ((triple10 triple8) -> rule6) OR ((triple8 triple6) -> rule2))] Charlie is furry.[(triple8 OR ((triple7 triple11) -> rule5))] Charlie is kind.[(triple9 OR ((triple12) -> rule3) OR ((triple10 triple6) -> rule1) OR ((((triple7) -> rule4)) -> rule3) OR ((((((triple10 triple8) -> rule6)) -> rule4)) -> rule3) OR ((((((triple8 triple6) -> rule2)) -> rule4)) -> rule3))] Charlie is nice.[(triple10)] Charlie is quiet.[(triple11)] Charlie is white.[(triple12 OR ((triple7) -> rule4) OR ((((triple10 triple8) -> rule6)) -> rule4) OR ((((triple8 triple6) -> rule2)) -> rule4))] Harry is furry.[(triple13)] Harry is nice.[(triple14)] Harry is quiet.[(triple15)] @1: Bob is kind.[(((triple5) -> rule3) OR ((((triple2) -> rule4)) -> rule3) OR ((((((triple3 triple1) -> rule2)) -> rule4)) -> rule3))] Harry is cold.[(((triple14 triple13) -> rule6))] @2: Harry is white.[(((((triple14 triple13) -> rule6)) -> rule4))] @3: Harry is kind.[(((((((triple14 triple13) -> rule6)) -> rule4)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple3 triple1) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple3
((triple2 triple4) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
((triple2) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple3 triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
((triple10 triple8) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple8 triple6) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
((triple7 triple11) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple9
((triple12) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple10 triple6) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((((triple10 triple8) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((((triple8 triple6) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple10
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple11
Charlie is white.
("Charlie" "is" "white" "+")
triple12
((triple7) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple10 triple8) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple8 triple6) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple13
Harry is nice.
("Harry" "is" "nice" "+")
triple14
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15
Bob is kind.
("Bob" "is" "kind" "+")
((triple5) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((((triple3 triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
((triple14 triple13) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((((triple14 triple13) -> (rule6 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((((triple14 triple13) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3