Dave is blue. Dave is white. Erin is red. Blue, green things are red. If Erin is smart and Erin is white then Erin is red. If Dave is big and Dave is blue then Dave is rough. All red things are rough. If Dave is white then Dave is green. Blue things are white.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is red.
("Erin" "is" "red" "+")
Blue, green things are red.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If Erin is smart and Erin is white then Erin is red.
((("Erin" "is" "smart" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "red" "+"))
If Dave is big and Dave is blue then Dave is rough.
((("Dave" "is" "big" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "rough" "+"))
All red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If Dave is white then Dave is green.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "green" "+"))
Blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Dave is blue.
True
1
proof
[(triple1)]
("Dave" "is" "blue" "+")
triple1
Dave is not white.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule6))]
("Dave" "is" "white" "-")
triple2
((triple1) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
True
2
proof
[(((triple2) -> rule5) OR ((((triple1) -> rule6)) -> rule5))]
("Dave" "is" "green" "+")
((triple2) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Erin is not rough.
False
2
inv-proof
[(((triple3) -> rule4))]
("Erin" "is" "rough" "-")
((triple3) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Dave is blue.[(triple1)] Dave is white.[(triple2 OR ((triple1) -> rule6))] Erin is red.[(triple3)] @1: Dave is green.[(((triple2) -> rule5) OR ((((triple1) -> rule6)) -> rule5))] Erin is rough.[(((triple3) -> rule4))] @2: Dave is red.[(((triple1 ((triple2) -> rule5)) -> rule1) OR ((triple1 ((((triple1) -> rule6)) -> rule5)) -> rule1))] @3: Dave is rough.[(((((triple1 ((triple2) -> rule5)) -> rule1)) -> rule4) OR ((((triple1 ((((triple1) -> rule6)) -> rule5)) -> rule1)) -> rule4))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
((triple1) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((((triple1 ((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
((((triple1 ((((triple1) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4