Dave is quiet. Dave is smart. Gary is red. Quiet people are round. Furry, quiet people are cold. If someone is red then they are young. If Gary is cold and Gary is quiet then Gary is young. All young people are furry. All red people are quiet. Smart, quiet people are cold. If someone is quiet and young then they are furry.
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is red.
("Gary" "is" "red" "+")
Quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Furry, quiet people are cold.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If someone is red then they are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If Gary is cold and Gary is quiet then Gary is young.
((("Gary" "is" "cold" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "young" "+"))
All young people are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
All red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Smart, quiet people are cold.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If someone is quiet and young then they are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
Dave is quiet.
True
1
proof
[(triple1)]
("Dave" "is" "quiet" "+")
triple1
Gary is not red.
False
1
inv-proof
[(triple3)]
("Gary" "is" "red" "-")
triple3
Dave is cold.
True
3
proof
[(((triple2 triple1) -> rule7))]
("Dave" "is" "cold" "+")
((triple2 triple1) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
3
inv-proof
[(((triple2 triple1) -> rule7))]
("Dave" "is" "cold" "-")
((triple2 triple1) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Gary is round.
True
3
proof
[(((((triple3) -> rule6)) -> rule1))]
("Gary" "is" "round" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not furry.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule5) OR ((((triple3) -> rule6) ((triple3) -> rule3)) -> rule8))]
("Gary" "is" "furry" "-")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple3) -> (rule6 % int3)) ((triple3) -> (rule3 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is cold.
True
6
proof
[(((((((triple3) -> rule3)) -> rule5) ((triple3) -> rule6)) -> rule2) OR ((((((triple3) -> rule6) ((triple3) -> rule3)) -> rule8) ((triple3) -> rule6)) -> rule2))]
("Gary" "is" "cold" "+")
((((((triple3) -> (rule3 % int4))) -> (rule5 % int3)) ((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
((((((triple3) -> (rule6 % int4)) ((triple3) -> (rule3 % int3))) -> (rule8 % int2)) ((triple3) -> (rule6 % int4))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is not cold.
False
6
inv-proof
[(((((((triple3) -> rule3)) -> rule5) ((triple3) -> rule6)) -> rule2) OR ((((((triple3) -> rule6) ((triple3) -> rule3)) -> rule8) ((triple3) -> rule6)) -> rule2))]
("Gary" "is" "cold" "-")
((((((triple3) -> (rule3 % int4))) -> (rule5 % int3)) ((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
((((((triple3) -> (rule6 % int4)) ((triple3) -> (rule3 % int3))) -> (rule8 % int2)) ((triple3) -> (rule6 % int4))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Dave is not furry.
Unknown
inv-rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is young.
Unknown
rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "young" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Dave is quiet.[(triple1)] Dave is smart.[(triple2)] Gary is red.[(triple3)] @1: Dave is cold.[(((triple2 triple1) -> rule7))] Dave is round.[(((triple1) -> rule1))] Gary is quiet.[(((triple3) -> rule6))] Gary is young.[(((triple3) -> rule3))] @2: Gary is furry.[(((((triple3) -> rule3)) -> rule5) OR ((((triple3) -> rule6) ((triple3) -> rule3)) -> rule8))] Gary is round.[(((((triple3) -> rule6)) -> rule1))] @3: Gary is cold.[(((((((triple3) -> rule3)) -> rule5) ((triple3) -> rule6)) -> rule2) OR ((((((triple3) -> rule6) ((triple3) -> rule3)) -> rule8) ((triple3) -> rule6)) -> rule2))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
((triple2 triple1) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple3) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple3) -> (rule6 % int3)) ((triple3) -> (rule3 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple3) -> (rule3 % int4))) -> (rule5 % int3)) ((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
((((((triple3) -> (rule6 % int4)) ((triple3) -> (rule3 % int3))) -> (rule8 % int2)) ((triple3) -> (rule6 % int4))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4