Anne is furry. Bob is rough. Harry is round. If Bob is rough then Bob is round. Young things are quiet. If Bob is quiet and Bob is young then Bob is white. If something is young then it is cold. Round things are quiet. White things are cold. Round things are cold. If Bob is round then Bob is young.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
If Bob is rough then Bob is round.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "round" "+"))
Young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If Bob is quiet and Bob is young then Bob is white.
((("Bob" "is" "quiet" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "white" "+"))
If something is young then it is cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
Round things are quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
White things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If Bob is round then Bob is young.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "young" "+"))
Harry is round.
True
1
proof
[(triple3)]
("Harry" "is" "round" "+")
triple3
Harry is not round.
False
1
inv-proof
[(triple3)]
("Harry" "is" "round" "-")
triple3
Harry is quiet.
True
2
proof
[(((triple3) -> rule5))]
("Harry" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple3) -> rule5))]
("Harry" "is" "quiet" "-")
((triple3) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Bob is cold.
True
3
proof
[(((((triple2) -> rule1)) -> rule7) OR ((((((triple2) -> rule1)) -> rule8)) -> rule4) OR ((((((((triple2) -> rule1)) -> rule5) ((((triple2) -> rule1)) -> rule8)) -> rule3)) -> rule6) OR ((((((((((triple2) -> rule1)) -> rule8)) -> rule2) ((((triple2) -> rule1)) -> rule8)) -> rule3)) -> rule6))]
("Bob" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((((triple2) -> (rule1 % int5))) -> (rule5 % int4)) ((((triple2) -> (rule1 % int5))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5
((((((((((triple2) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule2 % int3)) ((((triple2) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5
Bob is not cold.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule7) OR ((((((triple2) -> rule1)) -> rule8)) -> rule4) OR ((((((((triple2) -> rule1)) -> rule5) ((((triple2) -> rule1)) -> rule8)) -> rule3)) -> rule6) OR ((((((((((triple2) -> rule1)) -> rule8)) -> rule2) ((((triple2) -> rule1)) -> rule8)) -> rule3)) -> rule6))]
("Bob" "is" "cold" "-")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((((triple2) -> (rule1 % int5))) -> (rule5 % int4)) ((((triple2) -> (rule1 % int5))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5
((((((((((triple2) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule2 % int3)) ((((triple2) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5
Bob is white.
True
7
proof
[(((((((triple2) -> rule1)) -> rule5) ((((triple2) -> rule1)) -> rule8)) -> rule3) OR ((((((((triple2) -> rule1)) -> rule8)) -> rule2) ((((triple2) -> rule1)) -> rule8)) -> rule3))]
("Bob" "is" "white" "+")
((((((triple2) -> (rule1 % int4))) -> (rule5 % int3)) ((((triple2) -> (rule1 % int4))) -> (rule8 % int2))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
((((((((triple2) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule2 % int2)) ((((triple2) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is not white.
False
7
inv-proof
[(((((((triple2) -> rule1)) -> rule5) ((((triple2) -> rule1)) -> rule8)) -> rule3) OR ((((((((triple2) -> rule1)) -> rule8)) -> rule2) ((((triple2) -> rule1)) -> rule8)) -> rule3))]
("Bob" "is" "white" "-")
((((((triple2) -> (rule1 % int4))) -> (rule5 % int3)) ((((triple2) -> (rule1 % int4))) -> (rule8 % int2))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
((((((((triple2) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule2 % int2)) ((((triple2) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is cold.
Unknown
rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "cold" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Anne is furry.[(triple1)] Bob is rough.[(triple2)] Harry is round.[(triple3)] @1: Bob is round.[(((triple2) -> rule1))] Harry is cold.[(((triple3) -> rule7))] Harry is quiet.[(((triple3) -> rule5))] @2: Bob is cold.[(((((triple2) -> rule1)) -> rule7) OR ((((((triple2) -> rule1)) -> rule8)) -> rule4) OR ((((((((triple2) -> rule1)) -> rule5) ((((triple2) -> rule1)) -> rule8)) -> rule3)) -> rule6) OR ((((((((((triple2) -> rule1)) -> rule8)) -> rule2) ((((triple2) -> rule1)) -> rule8)) -> rule3)) -> rule6))] Bob is quiet.[(((((triple2) -> rule1)) -> rule5) OR ((((((triple2) -> rule1)) -> rule8)) -> rule2))] Bob is young.[(((((triple2) -> rule1)) -> rule8))] @3: Bob is white.[(((((((triple2) -> rule1)) -> rule5) ((((triple2) -> rule1)) -> rule8)) -> rule3) OR ((((((((triple2) -> rule1)) -> rule8)) -> rule2) ((((triple2) -> rule1)) -> rule8)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple3) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((((triple2) -> (rule1 % int5))) -> (rule5 % int4)) ((((triple2) -> (rule1 % int5))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5
((((((((((triple2) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule2 % int3)) ((((triple2) -> (rule1 % int5))) -> (rule8 % int4))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((((triple2) -> (rule1 % int4))) -> (rule5 % int3)) ((((triple2) -> (rule1 % int4))) -> (rule8 % int2))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
((((((((triple2) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule2 % int2)) ((((triple2) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4