Dave is quiet. Gary is cold. Harry is smart. If something is smart and green then it is big. All smart things are round. Big things are cold. If something is green then it is nice. Quiet things are big. If Dave is quiet and Dave is cold then Dave is nice. Smart things are round. If something is green then it is smart.
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is smart and green then it is big.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
All smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If something is green then it is nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If Dave is quiet and Dave is cold then Dave is nice.
((("Dave" "is" "quiet" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "nice" "+"))
Smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If something is green then it is smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Dave is quiet.
True
1
proof
[(triple1)]
("Dave" "is" "quiet" "+")
triple1
Dave is not quiet.
False
1
inv-proof
[(triple1)]
("Dave" "is" "quiet" "-")
triple1
Dave is big.
True
2
proof
[(((triple1) -> rule5))]
("Dave" "is" "big" "+")
((triple1) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple3) -> rule2) OR ((triple3) -> rule7))]
("Harry" "is" "round" "-")
((triple3) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple3) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Dave is cold.
True
3
proof
[(((((triple1) -> rule5)) -> rule3))]
("Dave" "is" "cold" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not cold.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3))]
("Dave" "is" "cold" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
True
5
proof
[(((triple1 ((((triple1) -> rule5)) -> rule3)) -> rule6))]
("Dave" "is" "nice" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not nice.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule5)) -> rule3)) -> rule6))]
("Dave" "is" "nice" "-")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "nice" "-")
Dave is round.
Unknown
rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("Dave" "is" "round" "+")
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "smart" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "smart" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Dave is quiet.[(triple1)] Gary is cold.[(triple2)] Harry is smart.[(triple3)] @1: Dave is big.[(((triple1) -> rule5))] Harry is round.[(((triple3) -> rule2) OR ((triple3) -> rule7))] @2: Dave is cold.[(((((triple1) -> rule5)) -> rule3))] @3: Dave is nice.[(((triple1 ((((triple1) -> rule5)) -> rule3)) -> rule6))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
((triple1) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple3) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple3) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3