Anne is blue. Anne is nice. Anne is quiet. Anne is smart. Anne is young. Bob is quiet. Bob is smart. Dave is blue. Dave is nice. Dave is quiet. Gary is nice. Gary is red. Blue, round things are smart. Smart, red things are round. If Bob is blue then Bob is round. If something is nice then it is quiet. If Gary is nice and Gary is quiet then Gary is smart. All blue things are young. If Gary is smart and Gary is round then Gary is blue. Smart things are round.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Blue, round things are smart.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
Smart, red things are round.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
If Bob is blue then Bob is round.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "round" "+"))
If something is nice then it is quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If Gary is nice and Gary is quiet then Gary is smart.
((("Gary" "is" "nice" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "smart" "+"))
All blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If Gary is smart and Gary is round then Gary is blue.
((("Gary" "is" "smart" "+") ("Gary" "is" "round" "+")) -> ("Gary" "is" "blue" "+"))
Smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Dave is blue.
True
1
proof
[(triple8)]
("Dave" "is" "blue" "+")
triple8
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Anne is round.
True
2
proof
[(((triple4) -> rule8))]
("Anne" "is" "round" "+")
((triple4) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple7) -> rule8))]
("Bob" "is" "round" "-")
((triple7) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Gary is smart.
True
4
proof
[(((triple11 ((triple11) -> rule4)) -> rule5))]
("Gary" "is" "smart" "+")
((triple11 ((triple11) -> (rule4 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not smart.
False
4
inv-proof
[(((triple11 ((triple11) -> rule4)) -> rule5))]
("Gary" "is" "smart" "-")
((triple11 ((triple11) -> (rule4 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is round.
True
5
proof
[(((((triple11 ((triple11) -> rule4)) -> rule5)) -> rule8) OR ((((triple11 ((triple11) -> rule4)) -> rule5) triple12) -> rule2))]
("Gary" "is" "round" "+")
((((triple11 ((triple11) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((triple11 ((triple11) -> (rule4 % int3))) -> (rule5 % int2)) triple12) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is not round.
False
5
inv-proof
[(((((triple11 ((triple11) -> rule4)) -> rule5)) -> rule8) OR ((((triple11 ((triple11) -> rule4)) -> rule5) triple12) -> rule2))]
("Gary" "is" "round" "-")
((((triple11 ((triple11) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((triple11 ((triple11) -> (rule4 % int3))) -> (rule5 % int2)) triple12) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is blue.
True
10
proof
[(((((triple11 ((triple11) -> rule4)) -> rule5) ((((triple11 ((triple11) -> rule4)) -> rule5)) -> rule8)) -> rule7) OR ((((triple11 ((triple11) -> rule4)) -> rule5) ((((triple11 ((triple11) -> rule4)) -> rule5) triple12) -> rule2)) -> rule7))]
("Gary" "is" "blue" "+")
((((triple11 ((triple11) -> (rule4 % int4))) -> (rule5 % int3)) ((((triple11 ((triple11) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
((((triple11 ((triple11) -> (rule4 % int4))) -> (rule5 % int3)) ((((triple11 ((triple11) -> (rule4 % int4))) -> (rule5 % int3)) triple12) -> (rule2 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is not blue.
False
10
inv-proof
[(((((triple11 ((triple11) -> rule4)) -> rule5) ((((triple11 ((triple11) -> rule4)) -> rule5)) -> rule8)) -> rule7) OR ((((triple11 ((triple11) -> rule4)) -> rule5) ((((triple11 ((triple11) -> rule4)) -> rule5) triple12) -> rule2)) -> rule7))]
("Gary" "is" "blue" "-")
((((triple11 ((triple11) -> (rule4 % int4))) -> (rule5 % int3)) ((((triple11 ((triple11) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
((((triple11 ((triple11) -> (rule4 % int4))) -> (rule5 % int3)) ((((triple11 ((triple11) -> (rule4 % int4))) -> (rule5 % int3)) triple12) -> (rule2 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is young.
True
11
proof
[(((((((triple11 ((triple11) -> rule4)) -> rule5) ((((triple11 ((triple11) -> rule4)) -> rule5)) -> rule8)) -> rule7)) -> rule6) OR ((((((triple11 ((triple11) -> rule4)) -> rule5) ((((triple11 ((triple11) -> rule4)) -> rule5) triple12) -> rule2)) -> rule7)) -> rule6))]
("Gary" "is" "young" "+")
((((((triple11 ((triple11) -> (rule4 % int5))) -> (rule5 % int4)) ((((triple11 ((triple11) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
((((((triple11 ((triple11) -> (rule4 % int5))) -> (rule5 % int4)) ((((triple11 ((triple11) -> (rule4 % int5))) -> (rule5 % int4)) triple12) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
Gary is not young.
False
11
inv-proof
[(((((((triple11 ((triple11) -> rule4)) -> rule5) ((((triple11 ((triple11) -> rule4)) -> rule5)) -> rule8)) -> rule7)) -> rule6) OR ((((((triple11 ((triple11) -> rule4)) -> rule5) ((((triple11 ((triple11) -> rule4)) -> rule5) triple12) -> rule2)) -> rule7)) -> rule6))]
("Gary" "is" "young" "-")
((((((triple11 ((triple11) -> (rule4 % int5))) -> (rule5 % int4)) ((((triple11 ((triple11) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
((((((triple11 ((triple11) -> (rule4 % int5))) -> (rule5 % int4)) ((((triple11 ((triple11) -> (rule4 % int5))) -> (rule5 % int4)) triple12) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "young" "-")
Dave is round.
Unknown
rconc
[@3: Dave is round.[CWA. Example of deepest failure = (rule8 <- rule1 <- rule2 <- FAIL)]]
("Dave" "is" "round" "+")
Dave is not smart.
Unknown
inv-rconc
[@2: Dave is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "smart" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Anne is blue.[(triple1)] Anne is nice.[(triple2)] Anne is quiet.[(triple3 OR ((triple2) -> rule4))] Anne is smart.[(triple4)] Anne is young.[(triple5 OR ((triple1) -> rule6))] Bob is quiet.[(triple6)] Bob is smart.[(triple7)] Dave is blue.[(triple8)] Dave is nice.[(triple9)] Dave is quiet.[(triple10 OR ((triple9) -> rule4))] Gary is nice.[(triple11)] Gary is red.[(triple12)] @1: Anne is round.[(((triple4) -> rule8))] Bob is round.[(((triple7) -> rule8))] Dave is young.[(((triple8) -> rule6))] Gary is quiet.[(((triple11) -> rule4))] @2: Gary is smart.[(((triple11 ((triple11) -> rule4)) -> rule5))] @3: Gary is round.[(((((triple11 ((triple11) -> rule4)) -> rule5)) -> rule8) OR ((((triple11 ((triple11) -> rule4)) -> rule5) triple12) -> rule2))] @4: Gary is blue.[(((((triple11 ((triple11) -> rule4)) -> rule5) ((((triple11 ((triple11) -> rule4)) -> rule5)) -> rule8)) -> rule7) OR ((((triple11 ((triple11) -> rule4)) -> rule5) ((((triple11 ((triple11) -> rule4)) -> rule5) triple12) -> rule2)) -> rule7))] @5: Gary is young.[(((((((triple11 ((triple11) -> rule4)) -> rule5) ((((triple11 ((triple11) -> rule4)) -> rule5)) -> rule8)) -> rule7)) -> rule6) OR ((((((triple11 ((triple11) -> rule4)) -> rule5) ((((triple11 ((triple11) -> rule4)) -> rule5) triple12) -> rule2)) -> rule7)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((triple2) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
((triple1) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is nice.
("Dave" "is" "nice" "+")
triple9
Dave is quiet.
("Dave" "is" "quiet" "+")
triple10
((triple9) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple11
Gary is red.
("Gary" "is" "red" "+")
triple12
Anne is round.
("Anne" "is" "round" "+")
((triple4) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple7) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple8) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple11) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple11 ((triple11) -> (rule4 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((triple11 ((triple11) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((triple11 ((triple11) -> (rule4 % int3))) -> (rule5 % int2)) triple12) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((((triple11 ((triple11) -> (rule4 % int4))) -> (rule5 % int3)) ((((triple11 ((triple11) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
((((triple11 ((triple11) -> (rule4 % int4))) -> (rule5 % int3)) ((((triple11 ((triple11) -> (rule4 % int4))) -> (rule5 % int3)) triple12) -> (rule2 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
((((((triple11 ((triple11) -> (rule4 % int5))) -> (rule5 % int4)) ((((triple11 ((triple11) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
((((((triple11 ((triple11) -> (rule4 % int5))) -> (rule5 % int4)) ((((triple11 ((triple11) -> (rule4 % int5))) -> (rule5 % int4)) triple12) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5