Dave is cold. Dave is smart. Gary is furry. Gary is smart. Gary is white. Harry is big. Harry is smart. Smart people are furry. If Dave is young then Dave is cold. White, furry people are smart. Blue people are big. All furry people are smart. If Dave is furry then Dave is blue. All furry people are white. If someone is big then they are furry.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If Dave is young then Dave is cold.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "cold" "+"))
White, furry people are smart.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
Blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
All furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If Dave is furry then Dave is blue.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "blue" "+"))
All furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If someone is big then they are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Gary is smart.
True
1
proof
[(triple4 OR ((triple3) -> rule5) OR ((triple5 triple3) -> rule3) OR ((((triple3) -> rule7) triple3) -> rule3))]
("Gary" "is" "smart" "+")
triple4
((triple3) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple5 triple3) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple3) -> (rule7 % int2)) triple3) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Harry is not smart.
False
1
inv-proof
[(triple7 OR ((((triple6) -> rule8)) -> rule5) OR ((((((triple6) -> rule8)) -> rule7) ((triple6) -> rule8)) -> rule3))]
("Harry" "is" "smart" "-")
triple7
((((triple6) -> (rule8 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple6) -> (rule8 % int3))) -> (rule7 % int2)) ((triple6) -> (rule8 % int3))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is furry.
True
2
proof
[(((triple6) -> rule8) OR ((triple7) -> rule1))]
("Harry" "is" "furry" "+")
((triple6) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple7) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple2) -> rule1))]
("Dave" "is" "furry" "-")
((triple2) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
True
3
proof
[(((((triple2) -> rule1)) -> rule7))]
("Dave" "is" "white" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6))]
("Dave" "is" "blue" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is big.
True
4
proof
[(((((((triple2) -> rule1)) -> rule6)) -> rule4))]
("Dave" "is" "big" "+")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not big.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule6)) -> rule4))]
("Dave" "is" "big" "-")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "big" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Dave is cold.[(triple1)] Dave is smart.[(triple2)] Gary is furry.[(triple3 OR ((triple4) -> rule1))] Gary is smart.[(triple4 OR ((triple3) -> rule5) OR ((triple5 triple3) -> rule3) OR ((((triple3) -> rule7) triple3) -> rule3))] Gary is white.[(triple5 OR ((triple3) -> rule7) OR ((((triple4) -> rule1)) -> rule7))] Harry is big.[(triple6)] Harry is smart.[(triple7 OR ((((triple6) -> rule8)) -> rule5) OR ((((((triple6) -> rule8)) -> rule7) ((triple6) -> rule8)) -> rule3))] @1: Dave is furry.[(((triple2) -> rule1))] Harry is furry.[(((triple6) -> rule8) OR ((triple7) -> rule1))] @2: Dave is blue.[(((((triple2) -> rule1)) -> rule6))] Dave is white.[(((((triple2) -> rule1)) -> rule7))] Harry is white.[(((((triple6) -> rule8)) -> rule7) OR ((((triple7) -> rule1)) -> rule7))] @3: Dave is big.[(((((((triple2) -> rule1)) -> rule6)) -> rule4))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
((triple4) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple4
((triple3) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple5 triple3) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple3) -> (rule7 % int2)) triple3) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple5
((triple3) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
((((triple6) -> (rule8 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple6) -> (rule8 % int3))) -> (rule7 % int2)) ((triple6) -> (rule8 % int3))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple6) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple7) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple6) -> (rule8 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3