Charlie is round. Dave is red. Gary is green. Gary is red. Gary is rough. Gary is white. Harry is red. If something is green and rough then it is red. If something is green then it is rough. Round things are green.
Charlie is round.
("Charlie" "is" "round" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is red.
("Harry" "is" "red" "+")
If something is green and rough then it is red.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something is green then it is rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Harry is red.
True
1
proof
[(triple7)]
("Harry" "is" "red" "+")
triple7
Gary is not green.
False
1
inv-proof
[(triple3)]
("Gary" "is" "green" "-")
triple3
Charlie is green.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "green" "+")
((triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "green" "-")
((triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not rough.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "rough" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is red.
True
6
proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule2)) -> rule1))]
("Charlie" "is" "red" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is not red.
False
6
inv-proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule2)) -> rule1))]
("Charlie" "is" "red" "-")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "green" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "green" "+")
Harry is not rough.
Unknown
inv-rconc
[@2: Harry is rough.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Harry" "is" "rough" "-")
Dave is rough.
Unknown
rconc
[@2: Dave is rough.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Dave" "is" "rough" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Charlie is round.[(triple1)] Dave is red.[(triple2)] Gary is green.[(triple3)] Gary is red.[(triple4 OR ((triple3 triple5) -> rule1) OR ((triple3 ((triple3) -> rule2)) -> rule1))] Gary is rough.[(triple5 OR ((triple3) -> rule2))] Gary is white.[(triple6)] Harry is red.[(triple7)] @1: Charlie is green.[(((triple1) -> rule3))] @2: Charlie is rough.[(((((triple1) -> rule3)) -> rule2))] @3: Charlie is red.[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule2)) -> rule1))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
triple4
((triple3 triple5) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple3 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
triple5
((triple3) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3