Bob is red. Bob is young. Dave is red. Gary is blue. Gary is smart. Harry is not nice. Harry is young. If Gary is big then Gary is blue. Blue, nice things are green. All green things are not young. If Dave is nice then Dave is big. All red things are smart. If something is young and not nice then it is red.
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is young.
("Harry" "is" "young" "+")
If Gary is big then Gary is blue.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "blue" "+"))
Blue, nice things are green.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
All green things are not young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "-"))
If Dave is nice then Dave is big.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "big" "+"))
All red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If something is young and not nice then it is red.
((("something" "is" "young" "+") ("something" "is" "nice" "~")) -> ("something" "is" "red" "+"))
Harry is young.
True
1
proof
[(triple7)]
("Harry" "is" "young" "+")
triple7
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Harry is red.
True
3
proof
[(((triple7 triple6) -> rule6))]
("Harry" "is" "red" "+")
((triple7 triple6) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
3
inv-proof
[(((triple7 triple6) -> rule6))]
("Harry" "is" "red" "-")
((triple7 triple6) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
True
4
proof
[(((((triple7 triple6) -> rule6)) -> rule5))]
("Harry" "is" "smart" "+")
((((triple7 triple6) -> (rule6 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not smart.
False
4
inv-proof
[(((((triple7 triple6) -> rule6)) -> rule5))]
("Harry" "is" "smart" "-")
((((triple7 triple6) -> (rule6 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "green" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "green" "+")
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Bob is red.[(triple1)] Bob is young.[(triple2)] Dave is red.[(triple3)] Gary is blue.[(triple4)] Gary is smart.[(triple5)] Harry is not nice.[(triple6)] Harry is young.[(triple7)] @1: Bob is smart.[(((triple1) -> rule5))] Dave is smart.[(((triple3) -> rule5))] Harry is red.[(((triple7 triple6) -> rule6))] @2: Harry is smart.[(((((triple7 triple6) -> rule6)) -> rule5))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Gary is smart.
("Gary" "is" "smart" "+")
triple5
Harry is not nice.
("Harry" "is" "nice" "-")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple3) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple7 triple6) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple7 triple6) -> (rule6 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2