Bob is red. Charlie is not blue. Gary is nice. If Bob is red then Bob is rough. If something is rough then it is big. If something is blue and not red then it is not big. If Gary is young then Gary is not smart. If Bob is big then Bob is smart. If something is young and red then it is not blue.
Bob is red.
("Bob" "is" "red" "+")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Gary is nice.
("Gary" "is" "nice" "+")
If Bob is red then Bob is rough.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "rough" "+"))
If something is rough then it is big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is blue and not red then it is not big.
((("something" "is" "blue" "+") ("something" "is" "red" "~")) -> ("something" "is" "big" "-"))
If Gary is young then Gary is not smart.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "smart" "-"))
If Bob is big then Bob is smart.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "smart" "+"))
If something is young and red then it is not blue.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "-"))
Bob is red.
True
1
proof
[(triple1)]
("Bob" "is" "red" "+")
triple1
Charlie is blue.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Bob is rough.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "rough" "-")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is smart.
True
4
proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule5))]
("Bob" "is" "smart" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not smart.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule5))]
("Bob" "is" "smart" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "big" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "big" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Bob is red.[(triple1)] Charlie is not blue.[(triple2)] Gary is nice.[(triple3)] @1: Bob is rough.[(((triple1) -> rule1))] @2: Bob is big.[(((((triple1) -> rule1)) -> rule2))] @3: Bob is smart.[(((((((triple1) -> rule1)) -> rule2)) -> rule5))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3