Anne is red. Charlie is red. Dave is kind. Dave is red. Dave is smart. Fiona is furry. Fiona is red. If Fiona is smart then Fiona is red. If something is smart then it is quiet. Red things are furry. If something is furry then it is quiet. If something is young then it is kind. All kind things are red. If Anne is furry and Anne is young then Anne is nice. All red, quiet things are smart.
Anne is red.
("Anne" "is" "red" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is red.
("Fiona" "is" "red" "+")
If Fiona is smart then Fiona is red.
((("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "red" "+"))
If something is smart then it is quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Red things are furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If something is furry then it is quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is young then it is kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If Anne is furry and Anne is young then Anne is nice.
((("Anne" "is" "furry" "+") ("Anne" "is" "young" "+")) -> ("Anne" "is" "nice" "+"))
All red, quiet things are smart.
((("something" "is" "red" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Dave is red.
True
1
proof
[(triple4 OR ((triple3) -> rule6))]
("Dave" "is" "red" "+")
triple4
((triple3) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Fiona is not furry.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule3))]
("Fiona" "is" "furry" "-")
triple6
((triple7) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is quiet.
True
2
proof
[(((triple6) -> rule4) OR ((((triple7) -> rule3)) -> rule4))]
("Fiona" "is" "quiet" "+")
((triple6) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Dave is not quiet.
False
2
inv-proof
[(((triple5) -> rule2) OR ((((triple4) -> rule3)) -> rule4) OR ((((((triple3) -> rule6)) -> rule3)) -> rule4))]
("Dave" "is" "quiet" "-")
((triple5) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Fiona is smart.
True
4
proof
[(((triple7 ((triple6) -> rule4)) -> rule8) OR ((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule8))]
("Fiona" "is" "smart" "+")
((triple7 ((triple6) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((triple7 ((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is not smart.
False
4
inv-proof
[(((triple7 ((triple6) -> rule4)) -> rule8) OR ((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule8))]
("Fiona" "is" "smart" "-")
((triple7 ((triple6) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((triple7 ((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Charlie is smart.
True
5
proof
[(((triple2 ((((triple2) -> rule3)) -> rule4)) -> rule8))]
("Charlie" "is" "smart" "+")
((triple2 ((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Anne is not smart.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule3)) -> rule4)) -> rule8))]
("Anne" "is" "smart" "-")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "kind" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "kind" "+")
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "nice" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Anne is red.[(triple1)] Charlie is red.[(triple2)] Dave is kind.[(triple3)] Dave is red.[(triple4 OR ((triple3) -> rule6))] Dave is smart.[(triple5 OR ((triple4 ((((triple4) -> rule3)) -> rule4)) -> rule8) OR ((((triple3) -> rule6) ((((triple4) -> rule3)) -> rule4)) -> rule8) OR ((triple4 ((((((triple3) -> rule6)) -> rule3)) -> rule4)) -> rule8) OR ((((triple3) -> rule6) ((((((triple3) -> rule6)) -> rule3)) -> rule4)) -> rule8))] Fiona is furry.[(triple6 OR ((triple7) -> rule3))] Fiona is red.[(triple7)] @1: Anne is furry.[(((triple1) -> rule3))] Charlie is furry.[(((triple2) -> rule3))] Dave is furry.[(((triple4) -> rule3) OR ((((triple3) -> rule6)) -> rule3))] Dave is quiet.[(((triple5) -> rule2) OR ((((triple4) -> rule3)) -> rule4) OR ((((((triple3) -> rule6)) -> rule3)) -> rule4))] Fiona is quiet.[(((triple6) -> rule4) OR ((((triple7) -> rule3)) -> rule4))] @2: Anne is quiet.[(((((triple1) -> rule3)) -> rule4))] Charlie is quiet.[(((((triple2) -> rule3)) -> rule4))] Fiona is smart.[(((triple7 ((triple6) -> rule4)) -> rule8) OR ((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule8))] @3: Anne is smart.[(((triple1 ((((triple1) -> rule3)) -> rule4)) -> rule8))] Charlie is smart.[(((triple2 ((((triple2) -> rule3)) -> rule4)) -> rule8))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
((triple3) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple5
((triple4 ((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((((triple3) -> (rule6 % int4)) ((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
((triple4 ((((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
((((triple3) -> (rule6 % int4)) ((((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Fiona is furry.
("Fiona" "is" "furry" "+")
triple6
((triple7) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple7
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple4) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple5) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple6) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple7 ((triple6) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((triple7 ((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2 ((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3