Anne is big. Anne is young. Charlie is nice. Charlie is white. Charlie is young. Fiona is white. Harry is kind. Big things are nice. If something is nice then it is white. Young, blue things are kind. If something is blue and young then it is kind. All kind things are blue. If Anne is big and Anne is nice then Anne is blue.
Anne is big.
("Anne" "is" "big" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it is white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Young, blue things are kind.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is blue and young then it is kind.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If Anne is big and Anne is nice then Anne is blue.
((("Anne" "is" "big" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "blue" "+"))
Harry is kind.
True
1
proof
[(triple7)]
("Harry" "is" "kind" "+")
triple7
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is nice.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple7) -> rule5))]
("Harry" "is" "blue" "-")
((triple7) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Anne is white.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Anne" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not blue.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule6))]
("Anne" "is" "blue" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is kind.
True
6
proof
[(((triple2 ((triple1 ((triple1) -> rule1)) -> rule6)) -> rule3) OR ((((triple1 ((triple1) -> rule1)) -> rule6) triple2) -> rule4))]
("Anne" "is" "kind" "+")
((triple2 ((triple1 ((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not kind.
False
6
inv-proof
[(((triple2 ((triple1 ((triple1) -> rule1)) -> rule6)) -> rule3) OR ((((triple1 ((triple1) -> rule1)) -> rule6) triple2) -> rule4))]
("Anne" "is" "kind" "-")
((triple2 ((triple1 ((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Charlie is not kind.
Unknown
inv-rconc
[@3: Charlie is kind.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule4 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is blue.
Unknown
rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Charlie" "is" "blue" "+")
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is blue.
Unknown
rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Fiona" "is" "blue" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is young.[(triple2)] Charlie is nice.[(triple3)] Charlie is white.[(triple4 OR ((triple3) -> rule2))] Charlie is young.[(triple5)] Fiona is white.[(triple6)] Harry is kind.[(triple7)] @1: Anne is nice.[(((triple1) -> rule1))] Harry is blue.[(((triple7) -> rule5))] @2: Anne is blue.[(((triple1 ((triple1) -> rule1)) -> rule6))] Anne is white.[(((((triple1) -> rule1)) -> rule2))] @3: Anne is kind.[(((triple2 ((triple1 ((triple1) -> rule1)) -> rule6)) -> rule3) OR ((((triple1 ((triple1) -> rule1)) -> rule6) triple2) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
((triple3) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Fiona is white.
("Fiona" "is" "white" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple7) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((triple2 ((triple1 ((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3