Dave is not big. Dave is red. Fiona is big. Fiona is not cold. Fiona is not furry. Fiona is red. Fiona is smart. Gary is green. Gary is red. Gary is smart. All green things are smart. Smart things are not quiet. If something is furry then it is red. If something is quiet then it is cold. If something is green and not quiet then it is cold. If Gary is cold then Gary is not big.
Dave is not big.
("Dave" "is" "big" "-")
Dave is red.
("Dave" "is" "red" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is not cold.
("Fiona" "is" "cold" "-")
Fiona is not furry.
("Fiona" "is" "furry" "-")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Smart things are not quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "-"))
If something is furry then it is red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If something is quiet then it is cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If something is green and not quiet then it is cold.
((("something" "is" "green" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "cold" "+"))
If Gary is cold then Gary is not big.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "big" "-"))
Gary is red.
True
1
proof
[(triple9)]
("Gary" "is" "red" "+")
triple9
Fiona is not smart.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "smart" "-")
triple7
Gary is not quiet.
True
2
proof
[(((triple10) -> rule2) OR ((((triple8) -> rule1)) -> rule2))]
("Gary" "is" "quiet" "-")
((triple10) -> (rule2 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
False
2
inv-proof
[(((triple10) -> rule2) OR ((((triple8) -> rule1)) -> rule2))]
("Gary" "is" "quiet" "+")
((triple10) -> (rule2 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
True
4
proof
[(((triple8 ((triple10) -> rule2)) -> rule5) OR ((triple8 ((((triple8) -> rule1)) -> rule2)) -> rule5))]
("Gary" "is" "cold" "+")
((triple8 ((triple10) -> (rule2 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
int2
((triple8 ((((triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not cold.
False
4
inv-proof
[(((triple8 ((triple10) -> rule2)) -> rule5) OR ((triple8 ((((triple8) -> rule1)) -> rule2)) -> rule5))]
("Gary" "is" "cold" "-")
((triple8 ((triple10) -> (rule2 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
int2
((triple8 ((((triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not big.
True
5
proof
[(((((triple8 ((triple10) -> rule2)) -> rule5)) -> rule6) OR ((((triple8 ((((triple8) -> rule1)) -> rule2)) -> rule5)) -> rule6))]
("Gary" "is" "big" "-")
((((triple8 ((triple10) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is not big.
("Gary" "is" "big" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not quiet.
("Gary" "is" "quiet" "-")
int3
((((triple8 ((((triple8) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is not big.
("Gary" "is" "big" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not quiet.
("Gary" "is" "quiet" "-")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is big.
False
5
inv-proof
[(((((triple8 ((triple10) -> rule2)) -> rule5)) -> rule6) OR ((((triple8 ((((triple8) -> rule1)) -> rule2)) -> rule5)) -> rule6))]
("Gary" "is" "big" "+")
((((triple8 ((triple10) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is not big.
("Gary" "is" "big" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not quiet.
("Gary" "is" "quiet" "-")
int3
((((triple8 ((((triple8) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is not big.
("Gary" "is" "big" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not quiet.
("Gary" "is" "quiet" "-")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "cold" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Dave is not big.[(triple1)] Dave is red.[(triple2)] Fiona is big.[(triple3)] Fiona is not cold.[(triple4)] Fiona is not furry.[(triple5)] Fiona is red.[(triple6)] Fiona is smart.[(triple7)] Gary is green.[(triple8)] Gary is red.[(triple9)] Gary is smart.[(triple10 OR ((triple8) -> rule1))] @1: Fiona is not quiet.[(((triple7) -> rule2))] Gary is not quiet.[(((triple10) -> rule2) OR ((((triple8) -> rule1)) -> rule2))] @2: Gary is cold.[(((triple8 ((triple10) -> rule2)) -> rule5) OR ((triple8 ((((triple8) -> rule1)) -> rule2)) -> rule5))] @3: Gary is not big.[(((((triple8 ((triple10) -> rule2)) -> rule5)) -> rule6) OR ((((triple8 ((((triple8) -> rule1)) -> rule2)) -> rule5)) -> rule6))]
Dave is not big.
("Dave" "is" "big" "-")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Fiona is big.
("Fiona" "is" "big" "+")
triple3
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple4
Fiona is not furry.
("Fiona" "is" "furry" "-")
triple5
Fiona is red.
("Fiona" "is" "red" "+")
triple6
Fiona is smart.
("Fiona" "is" "smart" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
triple8
Gary is red.
("Gary" "is" "red" "+")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple10
((triple8) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
((triple7) -> (rule2 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
((triple10) -> (rule2 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((triple8 ((triple10) -> (rule2 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
int2
((triple8 ((((triple8) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not big.
("Gary" "is" "big" "-")
((((triple8 ((triple10) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is not big.
("Gary" "is" "big" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not quiet.
("Gary" "is" "quiet" "-")
int3
((((triple8 ((((triple8) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is not big.
("Gary" "is" "big" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not quiet.
("Gary" "is" "quiet" "-")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4