Charlie is red. Charlie is not round. Charlie is young. Dave is cold. Dave is not green. Gary is not cold. Gary is green. If someone is cold then they are big. If someone is young then they are big.
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is not green.
("Dave" "is" "green" "-")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is green.
("Gary" "is" "green" "+")
If someone is cold then they are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If someone is young then they are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
Charlie is young.
True
1
proof
[(triple3)]
("Charlie" "is" "young" "+")
triple3
Dave is green.
False
1
inv-proof
[(triple5)]
("Dave" "is" "green" "+")
triple5
Charlie is big.
True
2
proof
[(((triple3) -> rule2))]
("Charlie" "is" "big" "+")
((triple3) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple3) -> rule2))]
("Charlie" "is" "big" "-")
((triple3) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "big" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Charlie is not round.[(triple2)] Charlie is red.[(triple1)] Charlie is young.[(triple3)] Dave is cold.[(triple4)] Dave is not green.[(triple5)] Gary is green.[(triple7)] Gary is not cold.[(triple6)] @1: Charlie is big.[(((triple3) -> rule2))] Dave is big.[(((triple4) -> rule1))]
Charlie is not round.
("Charlie" "is" "round" "-")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is not green.
("Dave" "is" "green" "-")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple7
Gary is not cold.
("Gary" "is" "cold" "-")
triple6
Charlie is big.
("Charlie" "is" "big" "+")
((triple3) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple4) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1