Bob is not quiet. Charlie is not young. Erin is furry. Red, young things are white. If Bob is not quiet then Bob is white. All young things are red. Furry things are young. If Erin is furry then Erin is quiet. All rough things are not cold. If something is young and red then it is cold. If something is furry and not quiet then it is not rough.
Bob is not quiet.
("Bob" "is" "quiet" "-")
Charlie is not young.
("Charlie" "is" "young" "-")
Erin is furry.
("Erin" "is" "furry" "+")
Red, young things are white.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If Bob is not quiet then Bob is white.
((("Bob" "is" "quiet" "~")) -> ("Bob" "is" "white" "+"))
All young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
Furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If Erin is furry then Erin is quiet.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "quiet" "+"))
All rough things are not cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "-"))
If something is young and red then it is cold.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is furry and not quiet then it is not rough.
((("something" "is" "furry" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "rough" "-"))
Erin is furry.
True
1
proof
[(triple3)]
("Erin" "is" "furry" "+")
triple3
Bob is quiet.
False
1
inv-proof
[(triple1)]
("Bob" "is" "quiet" "+")
triple1
Erin is quiet.
True
2
proof
[(((triple3) -> rule5))]
("Erin" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple3) -> rule4))]
("Erin" "is" "young" "-")
((triple3) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
True
3
proof
[(((((triple3) -> rule4)) -> rule3))]
("Erin" "is" "red" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not red.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule3))]
("Erin" "is" "red" "-")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is cold.
True
6
proof
[(((((triple3) -> rule4) ((((triple3) -> rule4)) -> rule3)) -> rule7))]
("Erin" "is" "cold" "+")
((((triple3) -> (rule4 % int3)) ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not cold.
False
6
inv-proof
[(((((triple3) -> rule4) ((((triple3) -> rule4)) -> rule3)) -> rule7))]
("Erin" "is" "cold" "-")
((((triple3) -> (rule4 % int3)) ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "cold" "+")
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "young" "-")
Bob is red.
Unknown
rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Bob" "is" "red" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is not quiet.[(triple1)] Charlie is not young.[(triple2)] Erin is furry.[(triple3)] @1: Bob is white.[(((triple1) -> rule2))] Erin is quiet.[(((triple3) -> rule5))] Erin is young.[(((triple3) -> rule4))] @2: Erin is red.[(((((triple3) -> rule4)) -> rule3))] @3: Erin is cold.[(((((triple3) -> rule4) ((((triple3) -> rule4)) -> rule3)) -> rule7))] Erin is white.[(((((((triple3) -> rule4)) -> rule3) ((triple3) -> rule4)) -> rule1))]
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple1
Charlie is not young.
("Charlie" "is" "young" "-")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple3) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((triple3) -> (rule4 % int3)) ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((((((triple3) -> (rule4 % int3))) -> (rule3 % int2)) ((triple3) -> (rule4 % int3))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3