Charlie is young. Dave is round. Gary is cold. Cold things are young. If Charlie is young then Charlie is red. Cold, red things are white. If something is cold and green then it is round. If something is young then it is red. All cold, blue things are green.
Charlie is young.
("Charlie" "is" "young" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If Charlie is young then Charlie is red.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "red" "+"))
Cold, red things are white.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If something is cold and green then it is round.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If something is young then it is red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
All cold, blue things are green.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Dave is round.
True
1
proof
[(triple2)]
("Dave" "is" "round" "+")
triple2
Charlie is not young.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "young" "-")
triple1
Charlie is red.
True
2
proof
[(((triple1) -> rule2) OR ((triple1) -> rule5))]
("Charlie" "is" "red" "+")
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple1) -> rule5))]
("Charlie" "is" "red" "-")
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Gary is red.
True
3
proof
[(((((triple3) -> rule1)) -> rule5))]
("Gary" "is" "red" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not red.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule5))]
("Gary" "is" "red" "-")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not round.
Unknown
inv-rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Gary" "is" "round" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "round" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is young.[(triple1)] Dave is round.[(triple2)] Gary is cold.[(triple3)] @1: Charlie is red.[(((triple1) -> rule2) OR ((triple1) -> rule5))] Gary is young.[(((triple3) -> rule1))] @2: Gary is red.[(((((triple3) -> rule1)) -> rule5))] @3: Gary is white.[(((triple3 ((((triple3) -> rule1)) -> rule5)) -> rule3))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple1) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple3) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3