Dave is not big. Erin is young. Fiona is furry. Gary is cold. If something is big then it is cold. If something is green then it is furry. All young things are green. If something is furry and not big then it is green. All green, nice things are not quiet. Young things are quiet. All cold, young things are not nice. If Gary is cold then Gary is young.
Dave is not big.
("Dave" "is" "big" "-")
Erin is young.
("Erin" "is" "young" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If something is big then it is cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If something is green then it is furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
All young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is furry and not big then it is green.
((("something" "is" "furry" "+") ("something" "is" "big" "~")) -> ("something" "is" "green" "+"))
All green, nice things are not quiet.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "-"))
Young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
All cold, young things are not nice.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "-"))
If Gary is cold then Gary is young.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "young" "+"))
Gary is cold.
True
1
proof
[(triple4)]
("Gary" "is" "cold" "+")
triple4
Gary is not cold.
False
1
inv-proof
[(triple4)]
("Gary" "is" "cold" "-")
triple4
Erin is green.
True
2
proof
[(((triple2) -> rule3))]
("Erin" "is" "green" "+")
((triple2) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple2) -> rule3))]
("Erin" "is" "green" "-")
((triple2) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Gary is green.
True
3
proof
[(((((triple4) -> rule8)) -> rule3))]
("Gary" "is" "green" "+")
((((triple4) -> (rule8 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple4) -> rule8)) -> rule3))]
("Gary" "is" "green" "-")
((((triple4) -> (rule8 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is furry.
True
4
proof
[(((((((triple4) -> rule8)) -> rule3)) -> rule2))]
("Gary" "is" "furry" "+")
((((((triple4) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is not furry.
False
4
inv-proof
[(((((((triple4) -> rule8)) -> rule3)) -> rule2))]
("Gary" "is" "furry" "-")
((((((triple4) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "cold" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "green" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "green" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Dave is not big.[(triple1)] Erin is young.[(triple2)] Fiona is furry.[(triple3)] Gary is cold.[(triple4)] @1: Erin is green.[(((triple2) -> rule3))] Erin is quiet.[(((triple2) -> rule6))] Gary is young.[(((triple4) -> rule8))] @2: Erin is furry.[(((((triple2) -> rule3)) -> rule2))] Gary is green.[(((((triple4) -> rule8)) -> rule3))] Gary is not nice.[(((triple4 ((triple4) -> rule8)) -> rule7))] Gary is quiet.[(((((triple4) -> rule8)) -> rule6))] @3: Gary is furry.[(((((((triple4) -> rule8)) -> rule3)) -> rule2))]
Dave is not big.
("Dave" "is" "big" "-")
triple1
Erin is young.
("Erin" "is" "young" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
((triple2) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple2) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple4) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple4) -> (rule8 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not nice.
("Gary" "is" "nice" "-")
((triple4 ((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple4) -> (rule8 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((((triple4) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3