Dave is green. Erin is not big. Harry is quiet. If something is white and cold then it is big. All white, cold things are big. If something is cold then it is big. Quiet, white things are round. All white things are not round. All big, cold things are not red. If something is green then it is cold. Red, round things are not white.
Dave is green.
("Dave" "is" "green" "+")
Erin is not big.
("Erin" "is" "big" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is white and cold then it is big.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
All white, cold things are big.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Quiet, white things are round.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
All white things are not round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "-"))
All big, cold things are not red.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "-"))
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Red, round things are not white.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "-"))
Erin is not big.
True
1
proof
[(triple2)]
("Erin" "is" "big" "-")
triple2
Erin is big.
False
1
inv-proof
[(triple2)]
("Erin" "is" "big" "+")
triple2
Dave is cold.
True
2
proof
[(((triple1) -> rule7))]
("Dave" "is" "cold" "+")
((triple1) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple1) -> rule7))]
("Dave" "is" "cold" "-")
((triple1) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
True
3
proof
[(((((triple1) -> rule7)) -> rule3))]
("Dave" "is" "big" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule3))]
("Dave" "is" "big" "-")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not red.
True
6
proof
[(((((((triple1) -> rule7)) -> rule3) ((triple1) -> rule7)) -> rule6))]
("Dave" "is" "red" "-")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2)) ((triple1) -> (rule7 % int3))) -> (rule6 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is red.
False
6
inv-proof
[(((((((triple1) -> rule7)) -> rule3) ((triple1) -> rule7)) -> rule6))]
("Dave" "is" "red" "+")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2)) ((triple1) -> (rule7 % int3))) -> (rule6 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "cold" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "round" "+")
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is cold.
Unknown
rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "cold" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Dave is green.[(triple1)] Erin is not big.[(triple2)] Harry is quiet.[(triple3)] @1: Dave is cold.[(((triple1) -> rule7))] @2: Dave is big.[(((((triple1) -> rule7)) -> rule3))] @3: Dave is not red.[(((((((triple1) -> rule7)) -> rule3) ((triple1) -> rule7)) -> rule6))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Erin is not big.
("Erin" "is" "big" "-")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
((triple1) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not red.
("Dave" "is" "red" "-")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2)) ((triple1) -> (rule7 % int3))) -> (rule6 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3