Bob is blue. Bob is cold. Bob is furry. Dave is blue. Dave is cold. Dave is furry. Dave is kind. Dave is round. Dave is smart. Harry is blue. Harry is cold. Harry is furry. Harry is kind. Harry is round. Harry is smart. Harry is young. Kind things are smart. If something is furry and smart then it is round. Blue things are kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
Kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If something is furry and smart then it is round.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Harry is cold.
True
1
proof
[(triple11)]
("Harry" "is" "cold" "+")
triple11
Bob is not cold.
False
1
inv-proof
[(triple2)]
("Bob" "is" "cold" "-")
triple2
Bob is kind.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Bob" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not smart.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Bob" "is" "smart" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is round.
True
5
proof
[(((triple3 ((((triple1) -> rule3)) -> rule1)) -> rule2))]
("Bob" "is" "round" "+")
((triple3 ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not round.
False
5
inv-proof
[(((triple3 ((((triple1) -> rule3)) -> rule1)) -> rule2))]
("Bob" "is" "round" "-")
((triple3 ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is furry.[(triple3)] Dave is blue.[(triple4)] Dave is cold.[(triple5)] Dave is furry.[(triple6)] Dave is kind.[(triple7 OR ((triple4) -> rule3))] Dave is round.[(triple8 OR ((triple6 triple9) -> rule2) OR ((triple6 ((triple7) -> rule1)) -> rule2) OR ((triple6 ((((triple4) -> rule3)) -> rule1)) -> rule2))] Dave is smart.[(triple9 OR ((triple7) -> rule1) OR ((((triple4) -> rule3)) -> rule1))] Harry is blue.[(triple10)] Harry is cold.[(triple11)] Harry is furry.[(triple12)] Harry is kind.[(triple13 OR ((triple10) -> rule3))] Harry is round.[(triple14 OR ((triple12 triple15) -> rule2) OR ((triple12 ((triple13) -> rule1)) -> rule2) OR ((triple12 ((((triple10) -> rule3)) -> rule1)) -> rule2))] Harry is smart.[(triple15 OR ((triple13) -> rule1) OR ((((triple10) -> rule3)) -> rule1))] Harry is young.[(triple16)] @1: Bob is kind.[(((triple1) -> rule3))] @2: Bob is smart.[(((((triple1) -> rule3)) -> rule1))] @3: Bob is round.[(((triple3 ((((triple1) -> rule3)) -> rule1)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
((triple4) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple8
((triple6 triple9) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple6 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((triple6 ((((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
triple9
((triple7) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple11
Harry is furry.
("Harry" "is" "furry" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
triple13
((triple10) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple14
((triple12 triple15) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple12 ((triple13) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple12 ((((triple10) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
triple15
((triple13) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple16
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((triple3 ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3