Dave is kind. Dave is red. Dave is smart. Dave is white. Dave is young. Erin is kind. Erin is young. Harry is furry. Harry is kind. Harry is red. Harry is smart. Harry is young. If Harry is smart then Harry is red. If something is white then it is young. If something is kind then it is smart. Big things are furry. If Dave is smart and Dave is red then Dave is young. All young things are kind.
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is smart then Harry is red.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "red" "+"))
If something is white then it is young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If something is kind then it is smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Big things are furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If Dave is smart and Dave is red then Dave is young.
((("Dave" "is" "smart" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "young" "+"))
All young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
Harry is smart.
True
1
proof
[(triple11 OR ((triple9) -> rule3) OR ((((triple12) -> rule6)) -> rule3))]
("Harry" "is" "smart" "+")
triple11
((triple9) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple12) -> (rule6 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not red.
False
1
inv-proof
[(triple10 OR ((triple11) -> rule1) OR ((((triple9) -> rule3)) -> rule1) OR ((((((triple12) -> rule6)) -> rule3)) -> rule1))]
("Harry" "is" "red" "-")
triple10
((triple11) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((((triple12) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Erin is smart.
True
2
proof
[(((triple6) -> rule3) OR ((((triple7) -> rule6)) -> rule3))]
("Erin" "is" "smart" "+")
((triple6) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not smart.
False
2
inv-proof
[(((triple6) -> rule3) OR ((((triple7) -> rule6)) -> rule3))]
("Erin" "is" "smart" "-")
((triple6) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "furry" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "furry" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Dave is kind.[(triple1 OR ((triple5) -> rule6) OR ((((triple4) -> rule2)) -> rule6) OR ((((triple3 triple2) -> rule5)) -> rule6))] Dave is red.[(triple2)] Dave is smart.[(triple3 OR ((triple1) -> rule3) OR ((((triple5) -> rule6)) -> rule3) OR ((((((triple4) -> rule2)) -> rule6)) -> rule3))] Dave is white.[(triple4)] Dave is young.[(triple5 OR ((triple4) -> rule2) OR ((triple3 triple2) -> rule5) OR ((((triple1) -> rule3) triple2) -> rule5))] Erin is kind.[(triple6 OR ((triple7) -> rule6))] Erin is young.[(triple7)] Harry is furry.[(triple8)] Harry is kind.[(triple9 OR ((triple12) -> rule6))] Harry is red.[(triple10 OR ((triple11) -> rule1) OR ((((triple9) -> rule3)) -> rule1) OR ((((((triple12) -> rule6)) -> rule3)) -> rule1))] Harry is smart.[(triple11 OR ((triple9) -> rule3) OR ((((triple12) -> rule6)) -> rule3))] Harry is young.[(triple12)] @1: Erin is smart.[(((triple6) -> rule3) OR ((((triple7) -> rule6)) -> rule3))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
((triple5) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple3 triple2) -> (rule5 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
((triple1) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
triple4
Dave is young.
("Dave" "is" "young" "+")
triple5
((triple4) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple3 triple2) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple1) -> (rule3 % int2)) triple2) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple6
((triple7) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
((triple12) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple10
((triple11) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((((triple12) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
triple11
((triple9) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple12) -> (rule6 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple12
Erin is smart.
("Erin" "is" "smart" "+")
((triple6) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2