Charlie is big. Charlie is nice. Charlie is red. Charlie is smart. Charlie is young. Dave is big. Dave is cold. Dave is nice. Dave is red. Dave is rough. Dave is smart. Dave is young. All red people are nice. If Charlie is nice and Charlie is cold then Charlie is smart.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
All red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If Charlie is nice and Charlie is cold then Charlie is smart.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "smart" "+"))
Dave is nice.
True
1
proof
[(triple8 OR ((triple9) -> rule1))]
("Dave" "is" "nice" "+")
triple8
((triple9) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Charlie is not smart.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "smart" "-")
triple4
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is big.[(triple1)] Charlie is nice.[(triple2 OR ((triple3) -> rule1))] Charlie is red.[(triple3)] Charlie is smart.[(triple4)] Charlie is young.[(triple5)] Dave is big.[(triple6)] Dave is cold.[(triple7)] Dave is nice.[(triple8 OR ((triple9) -> rule1))] Dave is red.[(triple9)] Dave is rough.[(triple10)] Dave is smart.[(triple11)] Dave is young.[(triple12)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
((triple3) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is cold.
("Dave" "is" "cold" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
triple8
((triple9) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple9
Dave is rough.
("Dave" "is" "rough" "+")
triple10
Dave is smart.
("Dave" "is" "smart" "+")
triple11
Dave is young.
("Dave" "is" "young" "+")
triple12