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