Bob is not big. Bob is not young. Dave is blue. Dave is round. Fiona is blue. Fiona is red. Fiona is round. All blue, big people are not cold. If Dave is young then Dave is not cold. If someone is red then they are big. All red people are blue. All cold people are not red. If someone is red and young then they are round.
Bob is not big.
("Bob" "is" "big" "-")
Bob is not young.
("Bob" "is" "young" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
All blue, big people are not cold.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "-"))
If Dave is young then Dave is not cold.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "cold" "-"))
If someone is red then they are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
All red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
All cold people are not red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "-"))
If someone is red and young then they are round.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
Bob is not big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Fiona is not blue.
False
1
inv-proof
[(triple5 OR ((triple6) -> rule4))]
("Fiona" "is" "blue" "-")
triple5
((triple6) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
True
2
proof
[(((triple6) -> rule3))]
("Fiona" "is" "big" "+")
((triple6) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not big.
False
2
inv-proof
[(((triple6) -> rule3))]
("Fiona" "is" "big" "-")
((triple6) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not cold.
True
4
proof
[(((triple5 ((triple6) -> rule3)) -> rule1) OR ((((triple6) -> rule4) ((triple6) -> rule3)) -> rule1))]
("Fiona" "is" "cold" "-")
((triple5 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((triple6) -> (rule4 % int3)) ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is cold.
False
4
inv-proof
[(((triple5 ((triple6) -> rule3)) -> rule1) OR ((((triple6) -> rule4) ((triple6) -> rule3)) -> rule1))]
("Fiona" "is" "cold" "+")
((triple5 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((triple6) -> (rule4 % int3)) ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is round.
Unknown
rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "round" "+")
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "big" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Bob is not big.[(triple1)] Bob is not young.[(triple2)] Dave is blue.[(triple3)] Dave is round.[(triple4)] Fiona is blue.[(triple5 OR ((triple6) -> rule4))] Fiona is red.[(triple6)] Fiona is round.[(triple7)] @1: Fiona is big.[(((triple6) -> rule3))] @2: Fiona is not cold.[(((triple5 ((triple6) -> rule3)) -> rule1) OR ((((triple6) -> rule4) ((triple6) -> rule3)) -> rule1))]
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is not young.
("Bob" "is" "young" "-")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
((triple6) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple6
Fiona is round.
("Fiona" "is" "round" "+")
triple7
Fiona is big.
("Fiona" "is" "big" "+")
((triple6) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not cold.
("Fiona" "is" "cold" "-")
((triple5 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((triple6) -> (rule4 % int3)) ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3