Anne is blue. Anne is not red. Anne is young. Bob is young. Erin is not red. Fiona is blue. Fiona is nice. If someone is red and blue then they are big. If someone is nice then they are big. All blue, young people are cold. Red, nice people are not cold. If Erin is big and Erin is blue then Erin is nice. All cold, blue people are not red. Red people are nice. If someone is blue and big then they are young. If someone is big and not red then they are not smart.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is not red.
("Anne" "is" "red" "-")
Anne is young.
("Anne" "is" "young" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is not red.
("Erin" "is" "red" "-")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
If someone is red and blue then they are big.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If someone is nice then they are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
All blue, young people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Red, nice people are not cold.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "-"))
If Erin is big and Erin is blue then Erin is nice.
((("Erin" "is" "big" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "nice" "+"))
All cold, blue people are not red.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "-"))
Red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone is blue and big then they are young.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is big and not red then they are not smart.
((("someone" "is" "big" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "smart" "-"))
Fiona is nice.
True
1
proof
[(triple7)]
("Fiona" "is" "nice" "+")
triple7
Fiona is not blue.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "blue" "-")
triple6
Fiona is big.
True
2
proof
[(((triple7) -> rule2))]
("Fiona" "is" "big" "+")
((triple7) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Anne is not cold.
False
3
inv-proof
[(((triple1 triple3) -> rule3))]
("Anne" "is" "cold" "-")
((triple1 triple3) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Fiona is young.
True
4
proof
[(((triple6 ((triple7) -> rule2)) -> rule8))]
("Fiona" "is" "young" "+")
((triple6 ((triple7) -> (rule2 % int2))) -> (rule8 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not young.
False
4
inv-proof
[(((triple6 ((triple7) -> rule2)) -> rule8))]
("Fiona" "is" "young" "-")
((triple6 ((triple7) -> (rule2 % int2))) -> (rule8 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is cold.
True
6
proof
[(((triple6 ((triple6 ((triple7) -> rule2)) -> rule8)) -> rule3))]
("Fiona" "is" "cold" "+")
((triple6 ((triple6 ((triple7) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is not cold.
False
6
inv-proof
[(((triple6 ((triple6 ((triple7) -> rule2)) -> rule8)) -> rule3))]
("Fiona" "is" "cold" "-")
((triple6 ((triple6 ((triple7) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is not red.
True
8
proof
[(((((triple6 ((triple6 ((triple7) -> rule2)) -> rule8)) -> rule3) triple6) -> rule6))]
("Fiona" "is" "red" "-")
((((triple6 ((triple6 ((triple7) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule3 % int2)) triple6) -> (rule6 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is red.
False
8
inv-proof
[(((((triple6 ((triple6 ((triple7) -> rule2)) -> rule8)) -> rule3) triple6) -> rule6))]
("Fiona" "is" "red" "+")
((((triple6 ((triple6 ((triple7) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule3 % int2)) triple6) -> (rule6 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is not smart.
True
11
proof
[(((((triple7) -> rule2) ((((triple6 ((triple6 ((triple7) -> rule2)) -> rule8)) -> rule3) triple6) -> rule6)) -> rule9))]
("Fiona" "is" "smart" "-")
((((triple7) -> (rule2 % int5)) ((((triple6 ((triple6 ((triple7) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule3 % int3)) triple6) -> (rule6 % int2))) -> (rule9 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is not red.
("Fiona" "is" "red" "-")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
int5
Fiona is smart.
False
11
inv-proof
[(((((triple7) -> rule2) ((((triple6 ((triple6 ((triple7) -> rule2)) -> rule8)) -> rule3) triple6) -> rule6)) -> rule9))]
("Fiona" "is" "smart" "+")
((((triple7) -> (rule2 % int5)) ((((triple6 ((triple6 ((triple7) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule3 % int3)) triple6) -> (rule6 % int2))) -> (rule9 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is not red.
("Fiona" "is" "red" "-")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
int5
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "nice" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "nice" "+")
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "young" "-")
Erin is big.
Unknown
rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Erin" "is" "big" "+")
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "cold" "-")
Erin is cold.
Unknown
rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "cold" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Anne is not red.[(triple2 OR ((((triple1 triple3) -> rule3) triple1) -> rule6))] Anne is young.[(triple3)] Bob is young.[(triple4)] Erin is not red.[(triple5)] Fiona is blue.[(triple6)] Fiona is nice.[(triple7)] @1: Anne is cold.[(((triple1 triple3) -> rule3))] Fiona is big.[(((triple7) -> rule2))] @2: Fiona is young.[(((triple6 ((triple7) -> rule2)) -> rule8))] @3: Fiona is cold.[(((triple6 ((triple6 ((triple7) -> rule2)) -> rule8)) -> rule3))] @4: Fiona is not red.[(((((triple6 ((triple6 ((triple7) -> rule2)) -> rule8)) -> rule3) triple6) -> rule6))] @5: Fiona is not smart.[(((((triple7) -> rule2) ((((triple6 ((triple6 ((triple7) -> rule2)) -> rule8)) -> rule3) triple6) -> rule6)) -> rule9))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is not red.
("Anne" "is" "red" "-")
triple2
((((triple1 triple3) -> (rule3 % int2)) triple1) -> (rule6 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Erin is not red.
("Erin" "is" "red" "-")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
Anne is cold.
("Anne" "is" "cold" "+")
((triple1 triple3) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple7) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple6 ((triple7) -> (rule2 % int2))) -> (rule8 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple6 ((triple6 ((triple7) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is not red.
("Fiona" "is" "red" "-")
((((triple6 ((triple6 ((triple7) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule3 % int2)) triple6) -> (rule6 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is not smart.
("Fiona" "is" "smart" "-")
((((triple7) -> (rule2 % int5)) ((((triple6 ((triple6 ((triple7) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule3 % int3)) triple6) -> (rule6 % int2))) -> (rule9 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is not red.
("Fiona" "is" "red" "-")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
int5