Bob is big. Bob is blue. Bob is nice. Bob is red. Bob is rough. Bob is not young. Gary is big. Gary is green. Harry is not blue. Harry is green. Harry is not red. Harry is rough. Big, young things are not red. Young things are nice. If something is nice and not young then it is big. If something is red and not big then it is not blue. All young things are blue. All big, green things are blue. Blue things are green. If something is rough and nice then it is green.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not young.
("Bob" "is" "young" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is green.
("Harry" "is" "green" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Big, young things are not red.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "-"))
Young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is nice and not young then it is big.
((("something" "is" "nice" "+") ("something" "is" "young" "~")) -> ("something" "is" "big" "+"))
If something is red and not big then it is not blue.
((("something" "is" "red" "+") ("something" "is" "big" "~")) -> ("something" "is" "blue" "-"))
All young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
All big, green things are blue.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is rough and nice then it is green.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Bob is rough.
True
1
proof
[(triple5)]
("Bob" "is" "rough" "+")
triple5
Gary is not green.
False
1
inv-proof
[(triple8)]
("Gary" "is" "green" "-")
triple8
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "nice" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Bob is big.[(triple1 OR ((triple3 triple6) -> rule3))] Bob is blue.[(triple2 OR ((triple1 ((triple5 triple3) -> rule8)) -> rule6) OR ((((triple3 triple6) -> rule3) ((triple5 triple3) -> rule8)) -> rule6))] Bob is nice.[(triple3)] Bob is not young.[(triple6)] Bob is red.[(triple4)] Bob is rough.[(triple5)] Gary is big.[(triple7)] Gary is green.[(triple8)] Harry is green.[(triple10)] Harry is not blue.[(triple9)] Harry is not red.[(triple11)] Harry is rough.[(triple12)] @1: Bob is green.[(((triple2) -> rule7) OR ((triple5 triple3) -> rule8))] Gary is blue.[(((triple7 triple8) -> rule6))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3 triple6) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple1 ((triple5 triple3) -> (rule8 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple3 triple6) -> (rule3 % int3)) ((triple5 triple3) -> (rule8 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not young.
("Bob" "is" "young" "-")
triple6
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is not blue.
("Harry" "is" "blue" "-")
triple9
Harry is not red.
("Harry" "is" "red" "-")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple5 triple3) -> (rule8 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple7 triple8) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1