Charlie is cold. Dave is big. Gary is rough. Harry is big. Big things are red. Green things are young. All cold things are rough.
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
All cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Charlie is cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "+")
triple1
Harry is not big.
False
1
inv-proof
[(triple4)]
("Harry" "is" "big" "-")
triple4
Charlie is rough.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple2) -> rule1))]
("Dave" "is" "red" "-")
((triple2) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "rough" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Charlie is cold.[(triple1)] Dave is big.[(triple2)] Gary is rough.[(triple3)] Harry is big.[(triple4)] @1: Charlie is rough.[(((triple1) -> rule3))] Dave is red.[(((triple2) -> rule1))] Harry is red.[(((triple4) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple2) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple4) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1