Bob is big. Bob is kind. Bob is red. Bob is smart. Bob is white. Gary is big. Gary is cold. Gary is green. Gary is kind. Gary is red. Gary is smart. Gary is white. Harry is big. Harry is green. Harry is kind. Harry is smart. Green, kind people are smart. If someone is green and red then they are cold. If someone is green and big then they are red. All red people are big. All green people are red. All smart people are cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Green, kind people are smart.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is green and red then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is green and big then they are red.
((("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
All green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
All smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
Bob is smart.
True
1
proof
[(triple4)]
("Bob" "is" "smart" "+")
triple4
Harry is not kind.
False
1
inv-proof
[(triple15)]
("Harry" "is" "kind" "-")
triple15
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Bob is big.[(triple1 OR ((triple3) -> rule4))] Bob is kind.[(triple2)] Bob is red.[(triple3)] Bob is smart.[(triple4)] Bob is white.[(triple5)] Gary is big.[(triple6 OR ((triple10) -> rule4) OR ((((triple8) -> rule5)) -> rule4))] Gary is cold.[(triple7 OR ((triple11) -> rule6) OR ((triple8 triple10) -> rule2) OR ((((triple8 triple9) -> rule1)) -> rule6) OR ((triple8 ((triple8) -> rule5)) -> rule2) OR ((triple8 ((triple8 triple6) -> rule3)) -> rule2))] Gary is green.[(triple8)] Gary is kind.[(triple9)] Gary is red.[(triple10 OR ((triple8) -> rule5) OR ((triple8 triple6) -> rule3))] Gary is smart.[(triple11 OR ((triple8 triple9) -> rule1))] Gary is white.[(triple12)] Harry is big.[(triple13 OR ((((triple14) -> rule5)) -> rule4))] Harry is green.[(triple14)] Harry is kind.[(triple15)] Harry is smart.[(triple16 OR ((triple14 triple15) -> rule1))] @1: Bob is cold.[(((triple4) -> rule6))] Harry is cold.[(((triple16) -> rule6) OR ((((triple14 triple15) -> rule1)) -> rule6) OR ((triple14 ((triple14) -> rule5)) -> rule2) OR ((triple14 ((triple14 triple13) -> rule3)) -> rule2))] Harry is red.[(((triple14) -> rule5) OR ((triple14 triple13) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
((triple10) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple7
((triple11) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple8 triple10) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple8 triple9) -> (rule1 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((triple8 ((triple8) -> (rule5 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((triple8 ((triple8 triple6) -> (rule3 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple10
((triple8) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple8 triple6) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple11
((triple8 triple9) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple12
Harry is big.
("Harry" "is" "big" "+")
triple13
((((triple14) -> (rule5 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple14
Harry is kind.
("Harry" "is" "kind" "+")
triple15
Harry is smart.
("Harry" "is" "smart" "+")
triple16
((triple14 triple15) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple4) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple16) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple14 triple15) -> (rule1 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple14 ((triple14) -> (rule5 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((triple14 ((triple14 triple13) -> (rule3 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((triple14) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple14 triple13) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1