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