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