Charlie is blue. Charlie is cold. Charlie is nice. Charlie is rough. Harry is blue. Harry is cold. Harry is kind. Harry is nice. Harry is red. Harry is rough. If Harry is kind then Harry is nice. Green, nice people are red. If Harry is rough then Harry is green. If someone is green and blue then they are red. All red, kind people are blue. All green people are rough.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Harry is kind then Harry is nice.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "nice" "+"))
Green, nice people are red.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If Harry is rough then Harry is green.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "green" "+"))
If someone is green and blue then they are red.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
All red, kind people are blue.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
All green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Harry is nice.
True
1
proof
[(triple8 OR ((triple7) -> rule1))]
("Harry" "is" "nice" "+")
triple8
((triple7) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not blue.
False
1
inv-proof
[(triple5 OR ((triple9 triple7) -> rule5) OR ((((((triple10) -> rule3) triple8) -> rule2) triple7) -> rule5) OR ((((((triple10) -> rule3) ((triple7) -> rule1)) -> rule2) triple7) -> rule5))]
("Harry" "is" "blue" "-")
triple5
((triple9 triple7) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((((triple10) -> (rule3 % int3)) triple8) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple10) -> (rule3 % int4)) ((triple7) -> (rule1 % int3))) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is green.
True
2
proof
[(((triple10) -> rule3))]
("Harry" "is" "green" "+")
((triple10) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple10) -> rule3))]
("Harry" "is" "green" "-")
((triple10) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Charlie is nice.[(triple3)] Charlie is rough.[(triple4)] Harry is blue.[(triple5 OR ((triple9 triple7) -> rule5) OR ((((((triple10) -> rule3) triple8) -> rule2) triple7) -> rule5) OR ((((((triple10) -> rule3) ((triple7) -> rule1)) -> rule2) triple7) -> rule5))] Harry is cold.[(triple6)] Harry is kind.[(triple7)] Harry is nice.[(triple8 OR ((triple7) -> rule1))] Harry is red.[(triple9 OR ((((triple10) -> rule3) triple5) -> rule4) OR ((((triple10) -> rule3) triple8) -> rule2) OR ((((triple10) -> rule3) ((triple7) -> rule1)) -> rule2))] Harry is rough.[(triple10)] @1: Harry is green.[(((triple10) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
triple5
((triple9 triple7) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((((triple10) -> (rule3 % int3)) triple8) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple10) -> (rule3 % int4)) ((triple7) -> (rule1 % int3))) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((triple7) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple9
((((triple10) -> (rule3 % int2)) triple5) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple10) -> (rule3 % int2)) triple8) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple10) -> (rule3 % int3)) ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
((triple10) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1