Anne is quiet. Dave is red. Erin is red. Gary is round. If Anne is big then Anne is rough. Rough, cold things are red. All big things are red. All cold things are red. All blue things are rough. All quiet, cold things are blue. Round things are not blue. If something is quiet then it is cold.
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Erin is red.
("Erin" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
If Anne is big then Anne is rough.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "rough" "+"))
Rough, cold things are red.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
All big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
All cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
All quiet, cold things are blue.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
Round things are not blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "-"))
If something is quiet then it is cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Erin is red.
True
1
proof
[(triple3)]
("Erin" "is" "red" "+")
triple3
Gary is not round.
False
1
inv-proof
[(triple4)]
("Gary" "is" "round" "-")
triple4
Anne is cold.
True
2
proof
[(((triple1) -> rule8))]
("Anne" "is" "cold" "+")
((triple1) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule8))]
("Anne" "is" "cold" "-")
((triple1) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
True
3
proof
[(((((triple1) -> rule8)) -> rule4) OR ((((((triple1 ((triple1) -> rule8)) -> rule6)) -> rule5) ((triple1) -> rule8)) -> rule2))]
("Anne" "is" "red" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((((triple1 ((triple1) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) ((triple1) -> (rule8 % int4))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is not blue.
False
4
inv-proof
[(((triple1 ((triple1) -> rule8)) -> rule6))]
("Anne" "is" "blue" "-")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is rough.
True
5
proof
[(((((triple1 ((triple1) -> rule8)) -> rule6)) -> rule5))]
("Anne" "is" "rough" "+")
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not rough.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule8)) -> rule6)) -> rule5))]
("Anne" "is" "rough" "-")
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "cold" "+")
Dave is not rough.
Unknown
inv-rconc
[@2: Dave is rough.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Dave" "is" "rough" "-")
Erin is rough.
Unknown
rconc
[@2: Erin is rough.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Erin" "is" "rough" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Anne is quiet.[(triple1)] Dave is red.[(triple2)] Erin is red.[(triple3)] Gary is round.[(triple4)] @1: Anne is cold.[(((triple1) -> rule8))] Gary is not blue.[(((triple4) -> rule7))] @2: Anne is blue.[(((triple1 ((triple1) -> rule8)) -> rule6))] Anne is red.[(((((triple1) -> rule8)) -> rule4) OR ((((((triple1 ((triple1) -> rule8)) -> rule6)) -> rule5) ((triple1) -> rule8)) -> rule2))] @3: Anne is rough.[(((((triple1 ((triple1) -> rule8)) -> rule6)) -> rule5))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Gary is not blue.
("Gary" "is" "blue" "-")
((triple4) -> (rule7 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((((triple1 ((triple1) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) ((triple1) -> (rule8 % int4))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3