Dave is big. If something is red and big then it is smart. If something is big and red then it is nice. If Dave is smart and Dave is big then Dave is nice. All green, white things are cold. If something is cold then it is smart. If something is big then it is nice. Nice, big things are smart. All white things are smart.
Dave is big.
("Dave" "is" "big" "+")
If something is red and big then it is smart.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If something is big and red then it is nice.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If Dave is smart and Dave is big then Dave is nice.
((("Dave" "is" "smart" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "nice" "+"))
All green, white things are cold.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If something is cold then it is smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is big then it is nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Nice, big things are smart.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
All white things are smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Dave is nice.
True
2
proof
[(((triple1) -> rule6))]
("Dave" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple1) -> rule6))]
("Dave" "is" "nice" "-")
((triple1) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
True
4
proof
[(((((triple1) -> rule6) triple1) -> rule7))]
("Dave" "is" "smart" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not smart.
False
4
inv-proof
[(((((triple1) -> rule6) triple1) -> rule7))]
("Dave" "is" "smart" "-")
((((triple1) -> (rule6 % int2)) triple1) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Dave is big.[(triple1)] @1: Dave is nice.[(((triple1) -> rule6))] @2: Dave is smart.[(((((triple1) -> rule6) triple1) -> rule7))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2