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