Anne is big. Anne is kind. Anne is rough. Anne is young. Bob is big. Bob is kind. Bob is rough. Charlie is rough. Fiona is blue. Fiona is rough. If someone is kind and blue then they are young. All kind people are rough. If someone is nice then they are big. If someone is blue then they are nice. If someone is blue and young then they are cold. If Charlie is cold and Charlie is kind then Charlie is young. All rough, big people are kind. If someone is blue and big then they are kind.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If someone is kind and blue then they are young.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
All kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is nice then they are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is blue then they are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is blue and young then they are cold.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is cold and Charlie is kind then Charlie is young.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "young" "+"))
All rough, big people are kind.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue and big then they are kind.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Bob is big.
True
1
proof
[(triple5)]
("Bob" "is" "big" "+")
triple5
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Fiona is nice.
True
2
proof
[(((triple9) -> rule4))]
("Fiona" "is" "nice" "+")
((triple9) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not nice.
False
2
inv-proof
[(((triple9) -> rule4))]
("Fiona" "is" "nice" "-")
((triple9) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is big.
True
3
proof
[(((((triple9) -> rule4)) -> rule3))]
("Fiona" "is" "big" "+")
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not big.
False
3
inv-proof
[(((((triple9) -> rule4)) -> rule3))]
("Fiona" "is" "big" "-")
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is kind.
True
5
proof
[(((triple10 ((((triple9) -> rule4)) -> rule3)) -> rule7) OR ((triple9 ((((triple9) -> rule4)) -> rule3)) -> rule8))]
("Fiona" "is" "kind" "+")
((triple10 ((((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
((triple9 ((((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is not kind.
False
5
inv-proof
[(((triple10 ((((triple9) -> rule4)) -> rule3)) -> rule7) OR ((triple9 ((((triple9) -> rule4)) -> rule3)) -> rule8))]
("Fiona" "is" "kind" "-")
((triple10 ((((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
((triple9 ((((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is young.
True
7
proof
[(((((triple10 ((((triple9) -> rule4)) -> rule3)) -> rule7) triple9) -> rule1) OR ((((triple9 ((((triple9) -> rule4)) -> rule3)) -> rule8) triple9) -> rule1))]
("Fiona" "is" "young" "+")
((((triple10 ((((triple9) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) triple9) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
((((triple9 ((((triple9) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) triple9) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Fiona is not young.
False
7
inv-proof
[(((((triple10 ((((triple9) -> rule4)) -> rule3)) -> rule7) triple9) -> rule1) OR ((((triple9 ((((triple9) -> rule4)) -> rule3)) -> rule8) triple9) -> rule1))]
("Fiona" "is" "young" "-")
((((triple10 ((((triple9) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) triple9) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
((((triple9 ((((triple9) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) triple9) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Fiona is cold.
True
9
proof
[(((triple9 ((((triple10 ((((triple9) -> rule4)) -> rule3)) -> rule7) triple9) -> rule1)) -> rule5) OR ((triple9 ((((triple9 ((((triple9) -> rule4)) -> rule3)) -> rule8) triple9) -> rule1)) -> rule5))]
("Fiona" "is" "cold" "+")
((triple9 ((((triple10 ((((triple9) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule7 % int3)) triple9) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
((triple9 ((((triple9 ((((triple9) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3)) triple9) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
Fiona is not cold.
False
9
inv-proof
[(((triple9 ((((triple10 ((((triple9) -> rule4)) -> rule3)) -> rule7) triple9) -> rule1)) -> rule5) OR ((triple9 ((((triple9 ((((triple9) -> rule4)) -> rule3)) -> rule8) triple9) -> rule1)) -> rule5))]
("Fiona" "is" "cold" "-")
((triple9 ((((triple10 ((((triple9) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule7 % int3)) triple9) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
((triple9 ((((triple9 ((((triple9) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3)) triple9) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is big.
Unknown
rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "big" "+")
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "cold" "-")
Charlie is kind.
Unknown
rconc
[@3: Charlie is kind.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "kind" "+")
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "cold" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is big.[(triple1)] Anne is kind.[(triple2 OR ((triple3 triple1) -> rule7))] Anne is rough.[(triple3 OR ((triple2) -> rule2))] Anne is young.[(triple4)] Bob is big.[(triple5)] Bob is kind.[(triple6 OR ((triple7 triple5) -> rule7))] Bob is rough.[(triple7 OR ((triple6) -> rule2))] Charlie is rough.[(triple8)] Fiona is blue.[(triple9)] Fiona is rough.[(triple10 OR ((((triple9 ((((triple9) -> rule4)) -> rule3)) -> rule8)) -> rule2))] @1: Fiona is nice.[(((triple9) -> rule4))] @2: Fiona is big.[(((((triple9) -> rule4)) -> rule3))] @3: Fiona is kind.[(((triple10 ((((triple9) -> rule4)) -> rule3)) -> rule7) OR ((triple9 ((((triple9) -> rule4)) -> rule3)) -> rule8))] @4: Fiona is young.[(((((triple10 ((((triple9) -> rule4)) -> rule3)) -> rule7) triple9) -> rule1) OR ((((triple9 ((((triple9) -> rule4)) -> rule3)) -> rule8) triple9) -> rule1))] @5: Fiona is cold.[(((triple9 ((((triple10 ((((triple9) -> rule4)) -> rule3)) -> rule7) triple9) -> rule1)) -> rule5) OR ((triple9 ((((triple9 ((((triple9) -> rule4)) -> rule3)) -> rule8) triple9) -> rule1)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((triple3 triple1) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple3
((triple2) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
triple5
Bob is kind.
("Bob" "is" "kind" "+")
triple6
((triple7 triple5) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple7
((triple6) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
Fiona is rough.
("Fiona" "is" "rough" "+")
triple10
((((triple9 ((((triple9) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple9) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple10 ((((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
((triple9 ((((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
((((triple10 ((((triple9) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) triple9) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
((((triple9 ((((triple9) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) triple9) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple9 ((((triple10 ((((triple9) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule7 % int3)) triple9) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5
((triple9 ((((triple9 ((((triple9) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule8 % int3)) triple9) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is nice.
("Fiona" "is" "nice" "+")
int5