Anne is young. Bob is quiet. Bob is young. Charlie is nice. Charlie is quiet. Charlie is round. Gary is round. If something is young then it is blue. All nice, round things are furry. Round, blue things are nice. Blue things are young. All round things are quiet. If something is quiet then it is nice. All smart things are furry. All furry, round things are young.
Anne is young.
("Anne" "is" "young" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is round.
("Gary" "is" "round" "+")
If something is young then it is blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
All nice, round things are furry.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
Round, blue things are nice.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All round things are quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet then it is nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
All smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
All furry, round things are young.
((("something" "is" "furry" "+") ("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
Bob is young.
True
1
proof
[(triple3)]
("Bob" "is" "young" "+")
triple3
Charlie is not nice.
False
1
inv-proof
[(triple4 OR ((triple5) -> rule6) OR ((((triple6) -> rule5)) -> rule6))]
("Charlie" "is" "nice" "-")
triple4
((triple5) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is furry.
True
3
proof
[(((triple4 triple6) -> rule2) OR ((((triple5) -> rule6) triple6) -> rule2) OR ((((((triple6) -> rule5)) -> rule6) triple6) -> rule2))]
("Charlie" "is" "furry" "+")
((triple4 triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple5) -> (rule6 % int2)) triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule6 % int2)) triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Bob is not blue.
False
2
inv-proof
[(((triple3) -> rule1))]
("Bob" "is" "blue" "-")
((triple3) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Gary is nice.
True
3
proof
[(((((triple7) -> rule5)) -> rule6))]
("Gary" "is" "nice" "+")
((((triple7) -> (rule5 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not nice.
False
3
inv-proof
[(((((triple7) -> rule5)) -> rule6))]
("Gary" "is" "nice" "-")
((((triple7) -> (rule5 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
True
5
proof
[(((((((triple7) -> rule5)) -> rule6) triple7) -> rule2))]
("Gary" "is" "furry" "+")
((((((triple7) -> (rule5 % int3))) -> (rule6 % int2)) triple7) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Charlie is not blue.
False
6
inv-proof
[(((((((triple4 triple6) -> rule2) triple6) -> rule8)) -> rule1) OR ((((((((triple5) -> rule6) triple6) -> rule2) triple6) -> rule8)) -> rule1) OR ((((((((((triple6) -> rule5)) -> rule6) triple6) -> rule2) triple6) -> rule8)) -> rule1))]
("Charlie" "is" "blue" "-")
((((((triple4 triple6) -> (rule2 % int3)) triple6) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((((((triple5) -> (rule6 % int4)) triple6) -> (rule2 % int3)) triple6) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
((((((((((triple6) -> (rule5 % int5))) -> (rule6 % int4)) triple6) -> (rule2 % int3)) triple6) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int5
Gary is young.
True
7
proof
[(((((((((triple7) -> rule5)) -> rule6) triple7) -> rule2) triple7) -> rule8))]
("Gary" "is" "young" "+")
((((((((triple7) -> (rule5 % int4))) -> (rule6 % int3)) triple7) -> (rule2 % int2)) triple7) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is not young.
False
7
inv-proof
[(((((((((triple7) -> rule5)) -> rule6) triple7) -> rule2) triple7) -> rule8))]
("Gary" "is" "young" "-")
((((((((triple7) -> (rule5 % int4))) -> (rule6 % int3)) triple7) -> (rule2 % int2)) triple7) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is blue.
True
8
proof
[(((((((((((triple7) -> rule5)) -> rule6) triple7) -> rule2) triple7) -> rule8)) -> rule1))]
("Gary" "is" "blue" "+")
((((((((((triple7) -> (rule5 % int5))) -> (rule6 % int4)) triple7) -> (rule2 % int3)) triple7) -> (rule8 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
Gary is not blue.
False
8
inv-proof
[(((((((((((triple7) -> rule5)) -> rule6) triple7) -> rule2) triple7) -> rule8)) -> rule1))]
("Gary" "is" "blue" "-")
((((((((((triple7) -> (rule5 % int5))) -> (rule6 % int4)) triple7) -> (rule2 % int3)) triple7) -> (rule8 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
Anne is not nice.
Unknown
inv-rconc
[@2: Anne is nice.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "quiet" "-")
Bob is furry.
Unknown
rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "furry" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Anne is young.[(triple1)] Bob is quiet.[(triple2)] Bob is young.[(triple3)] Charlie is nice.[(triple4 OR ((triple5) -> rule6) OR ((((triple6) -> rule5)) -> rule6))] Charlie is quiet.[(triple5 OR ((triple6) -> rule5))] Charlie is round.[(triple6)] Gary is round.[(triple7)] @1: Anne is blue.[(((triple1) -> rule1))] Bob is blue.[(((triple3) -> rule1))] Bob is nice.[(((triple2) -> rule6))] Charlie is furry.[(((triple4 triple6) -> rule2) OR ((((triple5) -> rule6) triple6) -> rule2) OR ((((((triple6) -> rule5)) -> rule6) triple6) -> rule2))] Gary is quiet.[(((triple7) -> rule5))] @2: Charlie is young.[(((((triple4 triple6) -> rule2) triple6) -> rule8) OR ((((((triple5) -> rule6) triple6) -> rule2) triple6) -> rule8) OR ((((((((triple6) -> rule5)) -> rule6) triple6) -> rule2) triple6) -> rule8))] Gary is nice.[(((((triple7) -> rule5)) -> rule6))] @3: Charlie is blue.[(((((((triple4 triple6) -> rule2) triple6) -> rule8)) -> rule1) OR ((((((((triple5) -> rule6) triple6) -> rule2) triple6) -> rule8)) -> rule1) OR ((((((((((triple6) -> rule5)) -> rule6) triple6) -> rule2) triple6) -> rule8)) -> rule1))] Gary is furry.[(((((((triple7) -> rule5)) -> rule6) triple7) -> rule2))] @4: Gary is young.[(((((((((triple7) -> rule5)) -> rule6) triple7) -> rule2) triple7) -> rule8))] @5: Gary is blue.[(((((((((((triple7) -> rule5)) -> rule6) triple7) -> rule2) triple7) -> rule8)) -> rule1))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
((triple5) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
((triple6) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple4 triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple5) -> (rule6 % int2)) triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule6 % int2)) triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple7) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple4 triple6) -> (rule2 % int2)) triple6) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((((triple5) -> (rule6 % int3)) triple6) -> (rule2 % int2)) triple6) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((((((triple6) -> (rule5 % int4))) -> (rule6 % int3)) triple6) -> (rule2 % int2)) triple6) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Gary is nice.
("Gary" "is" "nice" "+")
((((triple7) -> (rule5 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((((triple4 triple6) -> (rule2 % int3)) triple6) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((((((triple5) -> (rule6 % int4)) triple6) -> (rule2 % int3)) triple6) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
((((((((((triple6) -> (rule5 % int5))) -> (rule6 % int4)) triple6) -> (rule2 % int3)) triple6) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int5
Gary is furry.
("Gary" "is" "furry" "+")
((((((triple7) -> (rule5 % int3))) -> (rule6 % int2)) triple7) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
((((((((triple7) -> (rule5 % int4))) -> (rule6 % int3)) triple7) -> (rule2 % int2)) triple7) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
((((((((((triple7) -> (rule5 % int5))) -> (rule6 % int4)) triple7) -> (rule2 % int3)) triple7) -> (rule8 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5