Charlie is cold. Charlie is green. Charlie is nice. Charlie is white. Fiona is big. Fiona is blue. Fiona is nice. Fiona is not white. Gary is blue. Gary is not cold. Gary is green. Gary is nice. If something is big then it is not cold. If Gary is big and Gary is cold then Gary is not smart. All smart things are blue. All green things are blue. Smart things are green. All blue, nice things are smart.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is not white.
("Fiona" "is" "white" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
If something is big then it is not cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "-"))
If Gary is big and Gary is cold then Gary is not smart.
((("Gary" "is" "big" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "smart" "-"))
All smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All blue, nice things are smart.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Gary is nice.
True
1
proof
[(triple12)]
("Gary" "is" "nice" "+")
triple12
Gary is not green.
False
1
inv-proof
[(triple11 OR ((((triple9 triple12) -> rule6)) -> rule5))]
("Gary" "is" "green" "-")
triple11
((((triple9 triple12) -> (rule6 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is smart.
True
3
proof
[(((triple9 triple12) -> rule6) OR ((((triple11) -> rule4) triple12) -> rule6))]
("Gary" "is" "smart" "+")
((triple9 triple12) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple11) -> (rule4 % int2)) triple12) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Fiona is not smart.
False
3
inv-proof
[(((triple6 triple7) -> rule6))]
("Fiona" "is" "smart" "-")
((triple6 triple7) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
True
4
proof
[(((((triple6 triple7) -> rule6)) -> rule5))]
("Fiona" "is" "green" "+")
((((triple6 triple7) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is not green.
False
4
inv-proof
[(((((triple6 triple7) -> rule6)) -> rule5))]
("Fiona" "is" "green" "-")
((((triple6 triple7) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is cold.[(triple1)] Charlie is green.[(triple2)] Charlie is nice.[(triple3)] Charlie is white.[(triple4)] Fiona is big.[(triple5)] Fiona is blue.[(triple6)] Fiona is nice.[(triple7)] Fiona is not white.[(triple8)] Gary is blue.[(triple9 OR ((triple11) -> rule4))] Gary is green.[(triple11 OR ((((triple9 triple12) -> rule6)) -> rule5))] Gary is nice.[(triple12)] Gary is not cold.[(triple10)] @1: Charlie is blue.[(((triple2) -> rule4))] Fiona is not cold.[(((triple5) -> rule1))] Fiona is smart.[(((triple6 triple7) -> rule6))] Gary is smart.[(((triple9 triple12) -> rule6) OR ((((triple11) -> rule4) triple12) -> rule6))] @2: Charlie is smart.[(((((triple2) -> rule4) triple3) -> rule6))] Fiona is green.[(((((triple6 triple7) -> rule6)) -> rule5))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
Fiona is not white.
("Fiona" "is" "white" "-")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
((triple11) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple11
((((triple9 triple12) -> (rule6 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple12
Gary is not cold.
("Gary" "is" "cold" "-")
triple10
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Fiona is not cold.
("Fiona" "is" "cold" "-")
((triple5) -> (rule1 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple6 triple7) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple9 triple12) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple11) -> (rule4 % int2)) triple12) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple2) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((((triple6 triple7) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2