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