Dave is young. Erin is green. Erin is red. Erin is white. Fiona is not furry. Fiona is green. Gary is not green. If someone is young then they are furry. If someone is white and furry then they are nice. If someone is young and green then they are red. If Dave is nice then Dave is cold. If someone is furry then they are green. All furry, nice people are green. If someone is nice and not furry then they are green. If someone is green and furry then they are white.
Dave is young.
("Dave" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is not furry.
("Fiona" "is" "furry" "-")
Fiona is green.
("Fiona" "is" "green" "+")
Gary is not green.
("Gary" "is" "green" "-")
If someone is young then they are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If someone is white and furry then they are nice.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is young and green then they are red.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If Dave is nice then Dave is cold.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "cold" "+"))
If someone is furry then they are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
All furry, nice people are green.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is nice and not furry then they are green.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "green" "+"))
If someone is green and furry then they are white.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
Dave is young.
True
1
proof
[(triple1)]
("Dave" "is" "young" "+")
triple1
Gary is green.
False
1
inv-proof
[(triple7)]
("Gary" "is" "green" "+")
triple7
Dave is furry.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("Dave" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not green.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5))]
("Dave" "is" "green" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is red.
True
5
proof
[(((triple1 ((((triple1) -> rule1)) -> rule5)) -> rule3))]
("Dave" "is" "red" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not red.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule1)) -> rule5)) -> rule3))]
("Dave" "is" "red" "-")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is nice.
True
9
proof
[(((((((((triple1) -> rule1)) -> rule5) ((triple1) -> rule1)) -> rule8) ((triple1) -> rule1)) -> rule2))]
("Dave" "is" "nice" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule5 % int3)) ((triple1) -> (rule1 % int4))) -> (rule8 % int2)) ((triple1) -> (rule1 % int4))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is not nice.
False
9
inv-proof
[(((((((((triple1) -> rule1)) -> rule5) ((triple1) -> rule1)) -> rule8) ((triple1) -> rule1)) -> rule2))]
("Dave" "is" "nice" "-")
((((((((triple1) -> (rule1 % int4))) -> (rule5 % int3)) ((triple1) -> (rule1 % int4))) -> (rule8 % int2)) ((triple1) -> (rule1 % int4))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is cold.
True
10
proof
[(((((((((((triple1) -> rule1)) -> rule5) ((triple1) -> rule1)) -> rule8) ((triple1) -> rule1)) -> rule2)) -> rule4))]
("Dave" "is" "cold" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule5 % int4)) ((triple1) -> (rule1 % int5))) -> (rule8 % int3)) ((triple1) -> (rule1 % int5))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
int5
Dave is not cold.
False
10
inv-proof
[(((((((((((triple1) -> rule1)) -> rule5) ((triple1) -> rule1)) -> rule8) ((triple1) -> rule1)) -> rule2)) -> rule4))]
("Dave" "is" "cold" "-")
((((((((((triple1) -> (rule1 % int5))) -> (rule5 % int4)) ((triple1) -> (rule1 % int5))) -> (rule8 % int3)) ((triple1) -> (rule1 % int5))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
int5
Erin is not nice.
Unknown
inv-rconc
[@2: Erin is nice.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Erin" "is" "nice" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "nice" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "white" "+")
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "furry" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "white" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Dave is young.[(triple1)] Erin is green.[(triple2)] Erin is red.[(triple3)] Erin is white.[(triple4)] Fiona is green.[(triple6)] Fiona is not furry.[(triple5)] Gary is not green.[(triple7)] @1: Dave is furry.[(((triple1) -> rule1))] @2: Dave is green.[(((((triple1) -> rule1)) -> rule5))] @3: Dave is red.[(((triple1 ((((triple1) -> rule1)) -> rule5)) -> rule3))] Dave is white.[(((((((triple1) -> rule1)) -> rule5) ((triple1) -> rule1)) -> rule8))] @4: Dave is nice.[(((((((((triple1) -> rule1)) -> rule5) ((triple1) -> rule1)) -> rule8) ((triple1) -> rule1)) -> rule2))] @5: Dave is cold.[(((((((((((triple1) -> rule1)) -> rule5) ((triple1) -> rule1)) -> rule8) ((triple1) -> rule1)) -> rule2)) -> rule4))]
Dave is young.
("Dave" "is" "young" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Erin is white.
("Erin" "is" "white" "+")
triple4
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Fiona is not furry.
("Fiona" "is" "furry" "-")
triple5
Gary is not green.
("Gary" "is" "green" "-")
triple7
Dave is furry.
("Dave" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2)) ((triple1) -> (rule1 % int3))) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule5 % int3)) ((triple1) -> (rule1 % int4))) -> (rule8 % int2)) ((triple1) -> (rule1 % int4))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule5 % int4)) ((triple1) -> (rule1 % int5))) -> (rule8 % int3)) ((triple1) -> (rule1 % int5))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
int5