Bob is big. Dave is young. Fiona is quiet. All red things are big. If something is quiet and young then it is white. If something is white and not big then it is young. If something is quiet then it is young. If something is round and not white then it is not cold. Round things are not cold.
Bob is big.
("Bob" "is" "big" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
All red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is quiet and young then it is white.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If something is white and not big then it is young.
((("something" "is" "white" "+") ("something" "is" "big" "~")) -> ("something" "is" "young" "+"))
If something is quiet then it is young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
If something is round and not white then it is not cold.
((("something" "is" "round" "+") ("something" "is" "white" "~")) -> ("something" "is" "cold" "-"))
Round things are not cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "-"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Dave is not young.
False
1
inv-proof
[(triple2)]
("Dave" "is" "young" "-")
triple2
Fiona is young.
True
2
proof
[(((triple3) -> rule4))]
("Fiona" "is" "young" "+")
((triple3) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is not young.
False
2
inv-proof
[(((triple3) -> rule4))]
("Fiona" "is" "young" "-")
((triple3) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is white.
True
4
proof
[(((triple3 ((triple3) -> rule4)) -> rule2))]
("Fiona" "is" "white" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not white.
False
4
inv-proof
[(((triple3 ((triple3) -> rule4)) -> rule2))]
("Fiona" "is" "white" "-")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "big" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "big" "+")
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "young" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Bob is big.[(triple1)] Dave is young.[(triple2)] Fiona is quiet.[(triple3)] @1: Fiona is young.[(((triple3) -> rule4))] @2: Fiona is white.[(((triple3 ((triple3) -> rule4)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple3
Fiona is young.
("Fiona" "is" "young" "+")
((triple3) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2