Bob is green. Charlie is round. Gary is cold. If someone is round then they are furry. If someone is round and not cold then they are young. Furry people are young. If Charlie is not round then Charlie is not young. If someone is furry and not young then they are green. Young people are green.
Bob is green.
("Bob" "is" "green" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If someone is round then they are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
If someone is round and not cold then they are young.
((("someone" "is" "round" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "young" "+"))
Furry people are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If Charlie is not round then Charlie is not young.
((("Charlie" "is" "round" "~")) -> ("Charlie" "is" "young" "-"))
If someone is furry and not young then they are green.
((("someone" "is" "furry" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "green" "+"))
Young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Gary is not cold.
False
1
inv-proof
[(triple3)]
("Gary" "is" "cold" "-")
triple3
Charlie is furry.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "furry" "-")
((triple2) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "young" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is green.
True
4
proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule6))]
("Charlie" "is" "green" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is not green.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule6))]
("Charlie" "is" "green" "-")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "furry" "-")
Bob is young.
Unknown
rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Bob" "is" "young" "+")
Gary is not young.
Unknown
inv-rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Gary" "is" "young" "-")
Bob is furry.
Unknown
rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "furry" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Bob is green.[(triple1)] Charlie is round.[(triple2)] Gary is cold.[(triple3)] @1: Charlie is furry.[(((triple2) -> rule1))] @2: Charlie is young.[(((((triple2) -> rule1)) -> rule3))] @3: Charlie is green.[(((((((triple2) -> rule1)) -> rule3)) -> rule6))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3