Anne is round. Anne is young. Bob is not nice. Bob is red. Fiona is round. Harry is cold. Harry is young. Round things are green. If something is cold then it is blue. If something is young and round then it is blue. If something is cold then it is not red. All cold, green things are not red. Blue things are young. All blue things are round. If something is young then it is cold.
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is red.
("Bob" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is young.
("Harry" "is" "young" "+")
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is cold then it is blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something is young and round then it is blue.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is cold then it is not red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "-"))
All cold, green things are not red.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "-"))
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is young then it is cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
Harry is cold.
True
1
proof
[(triple6 OR ((triple7) -> rule8))]
("Harry" "is" "cold" "+")
triple6
((triple7) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule8))]
("Harry" "is" "cold" "-")
triple6
((triple7) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Anne is cold.
True
2
proof
[(((triple2) -> rule8))]
("Anne" "is" "cold" "+")
((triple2) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple6) -> rule2) OR ((((triple7) -> rule8)) -> rule2))]
("Harry" "is" "blue" "-")
((triple6) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple7) -> (rule8 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is round.
True
3
proof
[(((((triple6) -> rule2)) -> rule7) OR ((((((triple7) -> rule8)) -> rule2)) -> rule7))]
("Harry" "is" "round" "+")
((((triple6) -> (rule2 % int2))) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((((triple7) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Anne is red.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule4) OR ((((triple2) -> rule8) ((triple1) -> rule1)) -> rule5) OR ((((triple2) -> rule8) ((((((((triple2) -> rule8)) -> rule2)) -> rule7)) -> rule1)) -> rule5))]
("Anne" "is" "red" "+")
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple2) -> (rule8 % int3)) ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((triple2) -> (rule8 % int5)) ((((((((triple2) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
int5
Harry is green.
True
4
proof
[(((((((triple6) -> rule2)) -> rule7)) -> rule1) OR ((((((((triple7) -> rule8)) -> rule2)) -> rule7)) -> rule1))]
("Harry" "is" "green" "+")
((((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((((triple7) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is not green.
False
4
inv-proof
[(((((((triple6) -> rule2)) -> rule7)) -> rule1) OR ((((((((triple7) -> rule8)) -> rule2)) -> rule7)) -> rule1))]
("Harry" "is" "green" "-")
((((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((((triple7) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Bob is not young.
Unknown
inv-rconc
[@3: Bob is young.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule8 <- FAIL)]]
("Bob" "is" "young" "-")
Bob is cold.
Unknown
rconc
[@3: Bob is cold.[CWA. Example of deepest failure = (rule8 <- rule6 <- rule2 <- FAIL)]]
("Bob" "is" "cold" "+")
Fiona is not young.
Unknown
inv-rconc
[@3: Fiona is young.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule8 <- FAIL)]]
("Fiona" "is" "young" "-")
Fiona is blue.
Unknown
rconc
[@4: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule6 <- rule3 <- FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Anne is round.[(triple1 OR ((((((triple2) -> rule8)) -> rule2)) -> rule7))] Anne is young.[(triple2)] Bob is not nice.[(triple3)] Bob is red.[(triple4)] Fiona is round.[(triple5)] Harry is cold.[(triple6 OR ((triple7) -> rule8))] Harry is young.[(triple7 OR ((((triple6) -> rule2)) -> rule6))] @1: Anne is blue.[(((triple2 triple1) -> rule3) OR ((((triple2) -> rule8)) -> rule2))] Anne is cold.[(((triple2) -> rule8))] Anne is green.[(((triple1) -> rule1) OR ((((((((triple2) -> rule8)) -> rule2)) -> rule7)) -> rule1))] Fiona is green.[(((triple5) -> rule1))] Harry is blue.[(((triple6) -> rule2) OR ((((triple7) -> rule8)) -> rule2))] Harry is not red.[(((triple6) -> rule4) OR ((((triple7) -> rule8)) -> rule4) OR ((triple6 ((((((triple6) -> rule2)) -> rule7)) -> rule1)) -> rule5) OR ((((triple7) -> rule8) ((((((triple6) -> rule2)) -> rule7)) -> rule1)) -> rule5) OR ((triple6 ((((((((triple7) -> rule8)) -> rule2)) -> rule7)) -> rule1)) -> rule5) OR ((((triple7) -> rule8) ((((((((triple7) -> rule8)) -> rule2)) -> rule7)) -> rule1)) -> rule5))] @2: Anne is not red.[(((((triple2) -> rule8)) -> rule4) OR ((((triple2) -> rule8) ((triple1) -> rule1)) -> rule5) OR ((((triple2) -> rule8) ((((((((triple2) -> rule8)) -> rule2)) -> rule7)) -> rule1)) -> rule5))] Harry is round.[(((((triple6) -> rule2)) -> rule7) OR ((((((triple7) -> rule8)) -> rule2)) -> rule7))] @3: Harry is green.[(((((((triple6) -> rule2)) -> rule7)) -> rule1) OR ((((((((triple7) -> rule8)) -> rule2)) -> rule7)) -> rule1))]
Anne is round.
("Anne" "is" "round" "+")
triple1
((((((triple2) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
triple2
Bob is not nice.
("Bob" "is" "nice" "-")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Fiona is round.
("Fiona" "is" "round" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
((triple7) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple7
((((triple6) -> (rule2 % int2))) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((triple2 triple1) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple2) -> (rule8 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((triple2) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((((((triple2) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
((triple5) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple6) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple7) -> (rule8 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not red.
("Harry" "is" "red" "-")
((triple6) -> (rule4 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
((((triple7) -> (rule8 % int2))) -> (rule4 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((triple6 ((((((triple6) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
((((triple7) -> (rule8 % int5)) ((((((triple6) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
((triple6 ((((((((triple7) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
((((triple7) -> (rule8 % int5)) ((((((((triple7) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
Anne is not red.
("Anne" "is" "red" "-")
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple2) -> (rule8 % int3)) ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((triple2) -> (rule8 % int5)) ((((((((triple2) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
int5
Harry is round.
("Harry" "is" "round" "+")
((((triple6) -> (rule2 % int2))) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((((triple7) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((((triple7) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4