Bob is big. Bob is cold. Bob is nice. Bob is quiet. Bob is red. Bob is round. Dave is red. Dave is young. Fiona is nice. Harry is cold. All big, red people are quiet. If someone is young and red then they are nice. If Harry is quiet and Harry is young then Harry is nice. Round, nice people are quiet. Red people are nice. Big people are nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is cold.
("Harry" "is" "cold" "+")
All big, red people are quiet.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If someone is young and red then they are nice.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If Harry is quiet and Harry is young then Harry is nice.
((("Harry" "is" "quiet" "+") ("Harry" "is" "young" "+")) -> ("Harry" "is" "nice" "+"))
Round, nice people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Harry is cold.
True
1
proof
[(triple10)]
("Harry" "is" "cold" "+")
triple10
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "quiet" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Bob is nice.[(triple3 OR ((triple1) -> rule6) OR ((triple5) -> rule5))] Bob is quiet.[(triple4 OR ((triple1 triple5) -> rule1) OR ((triple6 triple3) -> rule4) OR ((triple6 ((triple1) -> rule6)) -> rule4) OR ((triple6 ((triple5) -> rule5)) -> rule4))] Bob is red.[(triple5)] Bob is round.[(triple6)] Dave is red.[(triple7)] Dave is young.[(triple8)] Fiona is nice.[(triple9)] Harry is cold.[(triple10)] @1: Dave is nice.[(((triple7) -> rule5) OR ((triple8 triple7) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple1) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple5) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple1 triple5) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple6 triple3) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple6 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((triple6 ((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
triple8
Fiona is nice.
("Fiona" "is" "nice" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Dave is nice.
("Dave" "is" "nice" "+")
((triple7) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple8 triple7) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1