Anne is big. Anne is blue. Anne is green. Anne is white. Charlie is blue. Charlie is not nice. Dave is kind. Fiona is furry. Fiona is kind. Fiona is nice. Nice, big people are kind. Big people are kind. Kind, blue people are nice. If Dave is not big then Dave is green. If Charlie is furry then Charlie is not nice. If someone is big and nice then they are furry. If Anne is white and Anne is green then Anne is kind. If someone is nice and not white then they are green.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Nice, big people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Big people are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Kind, blue people are nice.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If Dave is not big then Dave is green.
((("Dave" "is" "big" "~")) -> ("Dave" "is" "green" "+"))
If Charlie is furry then Charlie is not nice.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "nice" "-"))
If someone is big and nice then they are furry.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
If Anne is white and Anne is green then Anne is kind.
((("Anne" "is" "white" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "kind" "+"))
If someone is nice and not white then they are green.
((("someone" "is" "nice" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "green" "+"))
Fiona is nice.
True
1
proof
[(triple10)]
("Fiona" "is" "nice" "+")
triple10
Charlie is nice.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "nice" "+")
triple6
Anne is kind.
True
2
proof
[(((triple1) -> rule2) OR ((triple4 triple3) -> rule7))]
("Anne" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple4 triple3) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple4 triple3) -> rule7))]
("Anne" "is" "kind" "-")
((triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple4 triple3) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
True
4
proof
[(((((triple1) -> rule2) triple2) -> rule3) OR ((((triple4 triple3) -> rule7) triple2) -> rule3))]
("Anne" "is" "nice" "+")
((((triple1) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple4 triple3) -> (rule7 % int2)) triple2) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not nice.
False
4
inv-proof
[(((((triple1) -> rule2) triple2) -> rule3) OR ((((triple4 triple3) -> rule7) triple2) -> rule3))]
("Anne" "is" "nice" "-")
((((triple1) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple4 triple3) -> (rule7 % int2)) triple2) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
True
6
proof
[(((triple1 ((((triple1) -> rule2) triple2) -> rule3)) -> rule6) OR ((triple1 ((((triple4 triple3) -> rule7) triple2) -> rule3)) -> rule6))]
("Anne" "is" "furry" "+")
((triple1 ((((triple1) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((triple1 ((((triple4 triple3) -> (rule7 % int3)) triple2) -> (rule3 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is not furry.
False
6
inv-proof
[(((triple1 ((((triple1) -> rule2) triple2) -> rule3)) -> rule6) OR ((triple1 ((((triple4 triple3) -> rule7) triple2) -> rule3)) -> rule6))]
("Anne" "is" "furry" "-")
((triple1 ((((triple1) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((triple1 ((((triple4 triple3) -> (rule7 % int3)) triple2) -> (rule3 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "nice" "+")
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "green" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is green.[(triple3)] Anne is white.[(triple4)] Charlie is blue.[(triple5)] Charlie is not nice.[(triple6)] Dave is kind.[(triple7)] Fiona is furry.[(triple8)] Fiona is kind.[(triple9)] Fiona is nice.[(triple10)] @1: Anne is kind.[(((triple1) -> rule2) OR ((triple4 triple3) -> rule7))] @2: Anne is nice.[(((((triple1) -> rule2) triple2) -> rule3) OR ((((triple4 triple3) -> rule7) triple2) -> rule3))] @3: Anne is furry.[(((triple1 ((((triple1) -> rule2) triple2) -> rule3)) -> rule6) OR ((triple1 ((((triple4 triple3) -> rule7) triple2) -> rule3)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
Fiona is kind.
("Fiona" "is" "kind" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple4 triple3) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple4 triple3) -> (rule7 % int2)) triple2) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 ((((triple1) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((triple1 ((((triple4 triple3) -> (rule7 % int3)) triple2) -> (rule3 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3