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