Dave is red. Dave is smart. Erin is cold. Erin is smart. Erin is young. Fiona is cold. Fiona is furry. Fiona is smart. Fiona is young. Gary is smart. If someone is smart and furry then they are red. Kind, smart people are red. If someone is red then they are cold. All quiet, young people are furry. If someone is smart then they are kind. If Erin is smart then Erin is cold.
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If someone is smart and furry then they are red.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Kind, smart people are red.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
All quiet, young people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
If Erin is smart then Erin is cold.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "cold" "+"))
Erin is young.
True
1
proof
[(triple5)]
("Erin" "is" "young" "+")
triple5
Fiona is not young.
False
1
inv-proof
[(triple9)]
("Fiona" "is" "young" "-")
triple9
Fiona is kind.
True
2
proof
[(((triple8) -> rule5))]
("Fiona" "is" "kind" "+")
((triple8) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not red.
False
3
inv-proof
[(((triple8 triple7) -> rule1) OR ((((triple8) -> rule5) triple8) -> rule2))]
("Fiona" "is" "red" "-")
((triple8 triple7) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple8) -> (rule5 % int2)) triple8) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Erin is red.
True
4
proof
[(((((triple4) -> rule5) triple4) -> rule2))]
("Erin" "is" "red" "+")
((((triple4) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Gary is not red.
False
4
inv-proof
[(((((triple10) -> rule5) triple10) -> rule2))]
("Gary" "is" "red" "-")
((((triple10) -> (rule5 % int2)) triple10) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
True
5
proof
[(((((((triple10) -> rule5) triple10) -> rule2)) -> rule3))]
("Gary" "is" "cold" "+")
((((((triple10) -> (rule5 % int3)) triple10) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is not cold.
False
5
inv-proof
[(((((((triple10) -> rule5) triple10) -> rule2)) -> rule3))]
("Gary" "is" "cold" "-")
((((((triple10) -> (rule5 % int3)) triple10) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "furry" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "furry" "+")
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "furry" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Dave is red.[(triple1 OR ((((triple2) -> rule5) triple2) -> rule2))] Dave is smart.[(triple2)] Erin is cold.[(triple3 OR ((triple4) -> rule6) OR ((((((triple4) -> rule5) triple4) -> rule2)) -> rule3))] Erin is smart.[(triple4)] Erin is young.[(triple5)] Fiona is cold.[(triple6 OR ((((triple8 triple7) -> rule1)) -> rule3) OR ((((((triple8) -> rule5) triple8) -> rule2)) -> rule3))] Fiona is furry.[(triple7)] Fiona is smart.[(triple8)] Fiona is young.[(triple9)] Gary is smart.[(triple10)] @1: Dave is cold.[(((triple1) -> rule3) OR ((((((triple2) -> rule5) triple2) -> rule2)) -> rule3))] Dave is kind.[(((triple2) -> rule5))] Erin is kind.[(((triple4) -> rule5))] Fiona is kind.[(((triple8) -> rule5))] Fiona is red.[(((triple8 triple7) -> rule1) OR ((((triple8) -> rule5) triple8) -> rule2))] Gary is kind.[(((triple10) -> rule5))] @2: Erin is red.[(((((triple4) -> rule5) triple4) -> rule2))] Gary is red.[(((((triple10) -> rule5) triple10) -> rule2))] @3: Gary is cold.[(((((((triple10) -> rule5) triple10) -> rule2)) -> rule3))]
Dave is red.
("Dave" "is" "red" "+")
triple1
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
((triple4) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((((triple4) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
((((triple8 triple7) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((((triple8) -> (rule5 % int3)) triple8) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
Fiona is smart.
("Fiona" "is" "smart" "+")
triple8
Fiona is young.
("Fiona" "is" "young" "+")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Dave is cold.
("Dave" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((((triple2) -> (rule5 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((triple2) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple4) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple8) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple8 triple7) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple8) -> (rule5 % int2)) triple8) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((triple10) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple4) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((triple10) -> (rule5 % int2)) triple10) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple10) -> (rule5 % int3)) triple10) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3