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