Bob is round. Charlie is cold. Erin is smart. Gary is not green. If someone is red and not quiet then they are furry. If Charlie is green then Charlie is smart. Smart, cold people are red. If someone is round then they are cold. If someone is red then they are cold. Round, cold people are smart.
Bob is round.
("Bob" "is" "round" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is not green.
("Gary" "is" "green" "-")
If someone is red and not quiet then they are furry.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "furry" "+"))
If Charlie is green then Charlie is smart.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "smart" "+"))
Smart, cold people are red.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is round then they are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Round, cold people are smart.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Erin is smart.
True
1
proof
[(triple3)]
("Erin" "is" "smart" "+")
triple3
Charlie is not cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "-")
triple2
Bob is cold.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "cold" "-")
((triple1) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule6))]
("Bob" "is" "smart" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not smart.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule6))]
("Bob" "is" "smart" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is red.
True
7
proof
[(((((triple1 ((triple1) -> rule4)) -> rule6) ((triple1) -> rule4)) -> rule3))]
("Bob" "is" "red" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule6 % int2)) ((triple1) -> (rule4 % int3))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not red.
False
7
inv-proof
[(((((triple1 ((triple1) -> rule4)) -> rule6) ((triple1) -> rule4)) -> rule3))]
("Bob" "is" "red" "-")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule6 % int2)) ((triple1) -> (rule4 % int3))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "furry" "-")
Gary is cold.
Unknown
rconc
[@3: Gary is cold.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule6 <- FAIL)]]
("Gary" "is" "cold" "+")
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "furry" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Bob is round.[(triple1)] Charlie is cold.[(triple2)] Erin is smart.[(triple3)] Gary is not green.[(triple4)] @1: Bob is cold.[(((triple1) -> rule4))] @2: Bob is smart.[(((triple1 ((triple1) -> rule4)) -> rule6))] @3: Bob is red.[(((((triple1 ((triple1) -> rule4)) -> rule6) ((triple1) -> rule4)) -> rule3))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Gary is not green.
("Gary" "is" "green" "-")
triple4
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule6 % int2)) ((triple1) -> (rule4 % int3))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3