Bob is green. Gary is furry. Gary is quiet. If something is furry then it is green. If something is cold then it is quiet. If something is green then it is big. If something is cold then it is young. If something is furry and big then it is cold. If Bob is big then Bob is quiet. If something is big then it is young. Quiet, young things are big.
Bob is green.
("Bob" "is" "green" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If something is furry then it is green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If something is cold then it is quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If something is green then it is big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is cold then it is young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If something is furry and big then it is cold.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If Bob is big then Bob is quiet.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "quiet" "+"))
If something is big then it is young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Quiet, young things are big.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Gary is furry.
True
1
proof
[(triple2)]
("Gary" "is" "furry" "+")
triple2
Bob is not green.
False
1
inv-proof
[(triple1)]
("Bob" "is" "green" "-")
triple1
Bob is big.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "big" "+")
((triple1) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not big.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "big" "-")
((triple1) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Gary is not big.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Gary" "is" "big" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
True
4
proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule7) OR ((((triple2 ((((triple2) -> rule1)) -> rule3)) -> rule5)) -> rule4))]
("Gary" "is" "young" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((triple2 ((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is not young.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule7) OR ((((triple2 ((((triple2) -> rule1)) -> rule3)) -> rule5)) -> rule4))]
("Gary" "is" "young" "-")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((triple2 ((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "cold" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is green.[(triple1)] Gary is furry.[(triple2)] Gary is quiet.[(triple3 OR ((((triple2 ((((triple2) -> rule1)) -> rule3)) -> rule5)) -> rule2))] @1: Bob is big.[(((triple1) -> rule3))] Gary is green.[(((triple2) -> rule1))] @2: Bob is quiet.[(((((triple1) -> rule3)) -> rule6))] Bob is young.[(((((triple1) -> rule3)) -> rule7))] Gary is big.[(((((triple2) -> rule1)) -> rule3))] @3: Gary is cold.[(((triple2 ((((triple2) -> rule1)) -> rule3)) -> rule5))] Gary is young.[(((((((triple2) -> rule1)) -> rule3)) -> rule7) OR ((((triple2 ((((triple2) -> rule1)) -> rule3)) -> rule5)) -> rule4))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
((((triple2 ((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple2) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((((triple2 ((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4