Dave is kind. Erin is red. Red people are cold. Red people are young. If Erin is young and Erin is cold then Erin is furry. All nice, red people are young. Red, young people are cold. If someone is furry then they are cold.
Dave is kind.
("Dave" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If Erin is young and Erin is cold then Erin is furry.
((("Erin" "is" "young" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "furry" "+"))
All nice, red people are young.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Red, young people are cold.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is furry then they are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Erin is red.
True
1
proof
[(triple2)]
("Erin" "is" "red" "+")
triple2
Dave is not kind.
False
1
inv-proof
[(triple1)]
("Dave" "is" "kind" "-")
triple1
Erin is cold.
True
2
proof
[(((triple2) -> rule1) OR ((triple2 ((triple2) -> rule2)) -> rule5))]
("Erin" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not young.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "young" "-")
((triple2) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
True
5
proof
[(((((triple2) -> rule2) ((triple2) -> rule1)) -> rule3) OR ((((triple2) -> rule2) ((triple2 ((triple2) -> rule2)) -> rule5)) -> rule3))]
("Erin" "is" "furry" "+")
((((triple2) -> (rule2 % int3)) ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((triple2) -> (rule2 % int3)) ((triple2 ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not furry.
False
5
inv-proof
[(((((triple2) -> rule2) ((triple2) -> rule1)) -> rule3) OR ((((triple2) -> rule2) ((triple2 ((triple2) -> rule2)) -> rule5)) -> rule3))]
("Erin" "is" "furry" "-")
((((triple2) -> (rule2 % int3)) ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((triple2) -> (rule2 % int3)) ((triple2 ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is young.
Unknown
rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "young" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Dave is kind.[(triple1)] Erin is red.[(triple2)] @1: Erin is cold.[(((triple2) -> rule1) OR ((triple2 ((triple2) -> rule2)) -> rule5))] Erin is young.[(((triple2) -> rule2))] @2: Erin is furry.[(((((triple2) -> rule2) ((triple2) -> rule1)) -> rule3) OR ((((triple2) -> rule2) ((triple2 ((triple2) -> rule2)) -> rule5)) -> rule3))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((triple2) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple2) -> (rule2 % int3)) ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((triple2) -> (rule2 % int3)) ((triple2 ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3