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