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