Anne is quiet. Dave is big. Gary is cold. Harry is quiet. All quiet things are white. All quiet things are big. Big things are cold. If something is cold then it is rough. If Anne is green then Anne is quiet. If something is cold then it is white.
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All quiet things are white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
All quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
Big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If something is cold then it is rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If Anne is green then Anne is quiet.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "quiet" "+"))
If something is cold then it is white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Harry is not quiet.
False
1
inv-proof
[(triple4)]
("Harry" "is" "quiet" "-")
triple4
Gary is white.
True
2
proof
[(((triple3) -> rule6))]
("Gary" "is" "white" "+")
((triple3) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple1) -> rule1) OR ((((((triple1) -> rule2)) -> rule3)) -> rule6))]
("Anne" "is" "white" "-")
((triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is cold.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "cold" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "cold" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is rough.
True
4
proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule4))]
("Anne" "is" "rough" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not rough.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule4))]
("Anne" "is" "rough" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "big" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Anne is quiet.[(triple1)] Dave is big.[(triple2)] Gary is cold.[(triple3)] Harry is quiet.[(triple4)] @1: Anne is big.[(((triple1) -> rule2))] Anne is white.[(((triple1) -> rule1) OR ((((((triple1) -> rule2)) -> rule3)) -> rule6))] Dave is cold.[(((triple2) -> rule3))] Gary is rough.[(((triple3) -> rule4))] Gary is white.[(((triple3) -> rule6))] Harry is big.[(((triple4) -> rule2))] Harry is white.[(((triple4) -> rule1) OR ((((((triple4) -> rule2)) -> rule3)) -> rule6))] @2: Anne is cold.[(((((triple1) -> rule2)) -> rule3))] Dave is rough.[(((((triple2) -> rule3)) -> rule4))] Dave is white.[(((((triple2) -> rule3)) -> rule6))] Harry is cold.[(((((triple4) -> rule2)) -> rule3))] @3: Anne is rough.[(((((((triple1) -> rule2)) -> rule3)) -> rule4))] Harry is rough.[(((((((triple4) -> rule2)) -> rule3)) -> rule4))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
((triple2) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple4) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((((triple4) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
((((((triple4) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3