Anne is red. Dave is red. Erin is white. Fiona is white. If Fiona is smart then Fiona is white. All big people are white. If someone is red then they are big.
Anne is red.
("Anne" "is" "red" "+")
Dave is red.
("Dave" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If Fiona is smart then Fiona is white.
((("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "white" "+"))
All big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If someone is red then they are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Fiona is white.
True
1
proof
[(triple4)]
("Fiona" "is" "white" "+")
triple4
Dave is not red.
False
1
inv-proof
[(triple2)]
("Dave" "is" "red" "-")
triple2
Dave is big.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "big" "+")
((triple2) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "big" "-")
((triple2) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Anne is white.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "white" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Dave is not white.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("Dave" "is" "white" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "big" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "big" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Anne is red.[(triple1)] Dave is red.[(triple2)] Erin is white.[(triple3)] Fiona is white.[(triple4)] @1: Anne is big.[(((triple1) -> rule3))] Dave is big.[(((triple2) -> rule3))] @2: Anne is white.[(((((triple1) -> rule3)) -> rule2))] Dave is white.[(((((triple2) -> rule3)) -> rule2))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Fiona is white.
("Fiona" "is" "white" "+")
triple4
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2