Bob is kind. Bob is rough. Charlie is big. Charlie is green. Dave is white. Gary is big. Gary is cold. If someone is kind then they are cold. If someone is white then they are red. If someone is cold then they are big. Green, white people are red. White people are kind. If Dave is cold and Dave is rough then Dave is kind.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If someone is kind then they are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is white then they are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If someone is cold then they are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
Green, white people are red.
((("someone" "is" "green" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
White people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If Dave is cold and Dave is rough then Dave is kind.
((("Dave" "is" "cold" "+") ("Dave" "is" "rough" "+")) -> ("Dave" "is" "kind" "+"))
Gary is big.
True
1
proof
[(triple6 OR ((triple7) -> rule3))]
("Gary" "is" "big" "+")
triple6
((triple7) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Bob is not rough.
False
1
inv-proof
[(triple2)]
("Bob" "is" "rough" "-")
triple2
Bob is cold.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple5) -> rule5))]
("Dave" "is" "kind" "-")
((triple5) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
True
3
proof
[(((((triple5) -> rule5)) -> rule1))]
("Dave" "is" "cold" "+")
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not cold.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule1))]
("Dave" "is" "cold" "-")
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
True
4
proof
[(((((((triple5) -> rule5)) -> rule1)) -> rule3))]
("Dave" "is" "big" "+")
((((((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is not big.
False
4
inv-proof
[(((((((triple5) -> rule5)) -> rule1)) -> rule3))]
("Dave" "is" "big" "-")
((((((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "red" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "red" "+")
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "red" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "kind" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is kind.[(triple1)] Bob is rough.[(triple2)] Charlie is big.[(triple3)] Charlie is green.[(triple4)] Dave is white.[(triple5)] Gary is big.[(triple6 OR ((triple7) -> rule3))] Gary is cold.[(triple7)] @1: Bob is cold.[(((triple1) -> rule1))] Dave is kind.[(((triple5) -> rule5))] Dave is red.[(((triple5) -> rule2))] @2: Bob is big.[(((((triple1) -> rule1)) -> rule3))] Dave is cold.[(((((triple5) -> rule5)) -> rule1))] @3: Dave is big.[(((((((triple5) -> rule5)) -> rule1)) -> rule3))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
((triple7) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple5) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple5) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((((triple5) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3