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