Anne is white. Charlie is blue. Dave is round. Fiona is blue. If something is blue then it is round. If Fiona is round then Fiona is big. If something is red and white then it is big.
Anne is white.
("Anne" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
If something is blue then it is round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If Fiona is round then Fiona is big.
((("Fiona" "is" "round" "+")) -> ("Fiona" "is" "big" "+"))
If something is red and white then it is big.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Anne is not white.
False
1
inv-proof
[(triple1)]
("Anne" "is" "white" "-")
triple1
Charlie is round.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "round" "+")
((triple2) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Fiona is not round.
False
2
inv-proof
[(((triple4) -> rule1))]
("Fiona" "is" "round" "-")
((triple4) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
True
3
proof
[(((((triple4) -> rule1)) -> rule2))]
("Fiona" "is" "big" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is not big.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2))]
("Fiona" "is" "big" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "big" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "big" "+")
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "big" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
@0: Anne is white.[(triple1)] Charlie is blue.[(triple2)] Dave is round.[(triple3)] Fiona is blue.[(triple4)] @1: Charlie is round.[(((triple2) -> rule1))] Fiona is round.[(((triple4) -> rule1))] @2: Fiona is big.[(((((triple4) -> rule1)) -> rule2))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Fiona is blue.
("Fiona" "is" "blue" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
((triple2) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple4) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2