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