Anne is not furry. Charlie is smart. Fiona is furry. Gary is red. If Charlie is young and Charlie is round then Charlie is smart. Furry people are young. If someone is cold then they are round. If someone is smart then they are furry. If Charlie is green then Charlie is red. If Charlie is smart and Charlie is young then Charlie is not red.
Anne is not furry.
("Anne" "is" "furry" "-")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
If Charlie is young and Charlie is round then Charlie is smart.
((("Charlie" "is" "young" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "smart" "+"))
Furry people are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is smart then they are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If Charlie is green then Charlie is red.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "red" "+"))
If Charlie is smart and Charlie is young then Charlie is not red.
((("Charlie" "is" "smart" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "red" "-"))
Anne is not furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Charlie is not smart.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "smart" "-")
triple2
Fiona is young.
True
2
proof
[(((triple3) -> rule2))]
("Fiona" "is" "young" "+")
((triple3) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple2) -> rule4))]
("Charlie" "is" "furry" "-")
((triple2) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
True
3
proof
[(((((triple2) -> rule4)) -> rule2))]
("Charlie" "is" "young" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule2))]
("Charlie" "is" "young" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not red.
True
5
proof
[(((triple2 ((((triple2) -> rule4)) -> rule2)) -> rule6))]
("Charlie" "is" "red" "-")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is red.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule4)) -> rule2)) -> rule6))]
("Charlie" "is" "red" "+")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "round" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "furry" "+")
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "young" "-")
Gary is young.
Unknown
rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Gary" "is" "young" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Anne is not furry.[(triple1)] Charlie is smart.[(triple2)] Fiona is furry.[(triple3)] Gary is red.[(triple4)] @1: Charlie is furry.[(((triple2) -> rule4))] Fiona is young.[(((triple3) -> rule2))] @2: Charlie is young.[(((((triple2) -> rule4)) -> rule2))] @3: Charlie is not red.[(((triple2 ((((triple2) -> rule4)) -> rule2)) -> rule6))]
Anne is not furry.
("Anne" "is" "furry" "-")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple3) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not red.
("Charlie" "is" "red" "-")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3