Charlie is green. Harry is big. Harry is green. Green people are rough. All green people are blue. If someone is blue and rough then they are big.
Charlie is green.
("Charlie" "is" "green" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
All green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue and rough then they are big.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Harry is green.
True
1
proof
[(triple3)]
("Harry" "is" "green" "+")
triple3
Harry is not big.
False
1
inv-proof
[(triple2 OR ((((triple3) -> rule2) ((triple3) -> rule1)) -> rule3))]
("Harry" "is" "big" "-")
triple2
((((triple3) -> (rule2 % int3)) ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Charlie is rough.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "rough" "-")
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
True
5
proof
[(((((triple1) -> rule2) ((triple1) -> rule1)) -> rule3))]
("Charlie" "is" "big" "+")
((((triple1) -> (rule2 % int3)) ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is not big.
False
5
inv-proof
[(((((triple1) -> rule2) ((triple1) -> rule1)) -> rule3))]
("Charlie" "is" "big" "-")
((((triple1) -> (rule2 % int3)) ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is green.[(triple1)] Harry is big.[(triple2 OR ((((triple3) -> rule2) ((triple3) -> rule1)) -> rule3))] Harry is green.[(triple3)] @1: Charlie is blue.[(((triple1) -> rule2))] Charlie is rough.[(((triple1) -> rule1))] Harry is blue.[(((triple3) -> rule2))] Harry is rough.[(((triple3) -> rule1))] @2: Charlie is big.[(((((triple1) -> rule2) ((triple1) -> rule1)) -> rule3))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Harry is big.
("Harry" "is" "big" "+")
triple2
((((triple3) -> (rule2 % int3)) ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple3) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple1) -> (rule2 % int3)) ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3