Bob is cold. Bob is kind. Bob is red. Bob is smart. Bob is white. Harry is blue. Harry is cold. Harry is kind. Harry is nice. Harry is red. Harry is smart. Harry is white. If something is nice and white then it is cold. Red things are kind. If something is nice and cold then it is white. Kind, nice things are cold. If something is cold then it is red. Kind, smart things are red.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
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" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is nice and white then it is cold.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is nice and cold then it is white.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Kind, nice things are cold.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is cold then it is red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Kind, smart things are red.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Harry is white.
True
1
proof
[(triple12 OR ((triple9 triple7) -> rule3) OR ((triple9 ((triple8 triple9) -> rule4)) -> rule3) OR ((triple9 ((((triple10) -> rule2) triple9) -> rule4)) -> rule3))]
("Harry" "is" "white" "+")
triple12
((triple9 triple7) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple9 ((triple8 triple9) -> (rule4 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((triple9 ((((triple10) -> (rule2 % int3)) triple9) -> (rule4 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Bob is not red.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule5) OR ((triple2 triple4) -> rule6))]
("Bob" "is" "red" "-")
triple3
((triple1) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple2 triple4) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is cold.[(triple1)] Bob is kind.[(triple2 OR ((triple3) -> rule2) OR ((((triple1) -> rule5)) -> rule2))] Bob is red.[(triple3 OR ((triple1) -> rule5) OR ((triple2 triple4) -> rule6))] Bob is smart.[(triple4)] Bob is white.[(triple5)] Harry is blue.[(triple6)] Harry is cold.[(triple7 OR ((triple8 triple9) -> rule4) OR ((triple9 triple12) -> rule1) OR ((((triple10) -> rule2) triple9) -> rule4))] Harry is kind.[(triple8 OR ((triple10) -> rule2) OR ((((triple7) -> rule5)) -> rule2) OR ((((((triple9 triple12) -> rule1)) -> rule5)) -> rule2))] Harry is nice.[(triple9)] Harry is red.[(triple10 OR ((triple7) -> rule5) OR ((triple8 triple11) -> rule6) OR ((((triple8 triple9) -> rule4)) -> rule5) OR ((((triple9 triple12) -> rule1)) -> rule5))] Harry is smart.[(triple11)] Harry is white.[(triple12 OR ((triple9 triple7) -> rule3) OR ((triple9 ((triple8 triple9) -> rule4)) -> rule3) OR ((triple9 ((((triple10) -> rule2) triple9) -> rule4)) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
((triple3) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple3
((triple1) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple2 triple4) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
((triple8 triple9) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple9 triple12) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple10) -> (rule2 % int2)) triple9) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple8
((triple10) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((((triple9 triple12) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple10
((triple7) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple8 triple11) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple8 triple9) -> (rule4 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple9 triple12) -> (rule1 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
((triple9 triple7) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple9 ((triple8 triple9) -> (rule4 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((triple9 ((((triple10) -> (rule2 % int3)) triple9) -> (rule4 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3