Charlie is young. Erin is not smart. Gary is smart. Furry, smart things are young. If Gary is round and Gary is blue then Gary is red. All smart, furry things are nice. If something is smart then it is furry. Blue things are red. Furry, nice things are round.
Charlie is young.
("Charlie" "is" "young" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Gary is smart.
("Gary" "is" "smart" "+")
Furry, smart things are young.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If Gary is round and Gary is blue then Gary is red.
((("Gary" "is" "round" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "red" "+"))
All smart, furry things are nice.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is smart then it is furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Furry, nice things are round.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Erin is not smart.
True
1
proof
[(triple2)]
("Erin" "is" "smart" "-")
triple2
Charlie is not young.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "young" "-")
triple1
Gary is furry.
True
2
proof
[(((triple3) -> rule4))]
("Gary" "is" "furry" "+")
((triple3) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple3) -> rule4))]
("Gary" "is" "furry" "-")
((triple3) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
True
4
proof
[(((triple3 ((triple3) -> rule4)) -> rule3))]
("Gary" "is" "nice" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not young.
False
4
inv-proof
[(((((triple3) -> rule4) triple3) -> rule1))]
("Gary" "is" "young" "-")
((((triple3) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is round.
True
7
proof
[(((((triple3) -> rule4) ((triple3 ((triple3) -> rule4)) -> rule3)) -> rule6))]
("Gary" "is" "round" "+")
((((triple3) -> (rule4 % int3)) ((triple3 ((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is not round.
False
7
inv-proof
[(((((triple3) -> rule4) ((triple3 ((triple3) -> rule4)) -> rule3)) -> rule6))]
("Gary" "is" "round" "-")
((((triple3) -> (rule4 % int3)) ((triple3 ((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "young" "-")
Charlie is furry.
Unknown
rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is round.
Unknown
rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Charlie is young.[(triple1)] Erin is not smart.[(triple2)] Gary is smart.[(triple3)] @1: Gary is furry.[(((triple3) -> rule4))] @2: Gary is nice.[(((triple3 ((triple3) -> rule4)) -> rule3))] Gary is young.[(((((triple3) -> rule4) triple3) -> rule1))] @3: Gary is round.[(((((triple3) -> rule4) ((triple3 ((triple3) -> rule4)) -> rule3)) -> rule6))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Erin is not smart.
("Erin" "is" "smart" "-")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
((triple3) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((triple3) -> (rule4 % int3)) ((triple3 ((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3