Bob is quiet. Bob is smart. Charlie is blue. Charlie is furry. Charlie is red. Charlie is round. Fiona is blue. Fiona is quiet. Fiona is red. Fiona is smart. Gary is blue. Gary is furry. Gary is quiet. Gary is round. Gary is smart. All big people are blue. All round people are red. Red people are quiet. All quiet, red people are round. Quiet, smart people are round. All big, quiet people are blue.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All big people are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
All round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
All quiet, red people are round.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
Quiet, smart people are round.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
All big, quiet people are blue.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
Gary is quiet.
True
1
proof
[(triple13 OR ((((triple14) -> rule2)) -> rule3))]
("Gary" "is" "quiet" "+")
triple13
((((triple14) -> (rule2 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Bob is not smart.
False
1
inv-proof
[(triple2)]
("Bob" "is" "smart" "-")
triple2
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "blue" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Bob is quiet.[(triple1)] Bob is smart.[(triple2)] Charlie is blue.[(triple3)] Charlie is furry.[(triple4)] Charlie is red.[(triple5 OR ((triple6) -> rule2))] Charlie is round.[(triple6 OR ((((triple5) -> rule3) triple5) -> rule4))] Fiona is blue.[(triple7)] Fiona is quiet.[(triple8 OR ((triple9) -> rule3))] Fiona is red.[(triple9 OR ((((triple8 triple10) -> rule5)) -> rule2))] Fiona is smart.[(triple10)] Gary is blue.[(triple11)] Gary is furry.[(triple12)] Gary is quiet.[(triple13 OR ((((triple14) -> rule2)) -> rule3))] Gary is round.[(triple14 OR ((triple13 triple15) -> rule5))] Gary is smart.[(triple15)] @1: Bob is round.[(((triple1 triple2) -> rule5))] Charlie is quiet.[(((triple5) -> rule3) OR ((((triple6) -> rule2)) -> rule3))] Fiona is round.[(((triple8 triple10) -> rule5) OR ((triple8 triple9) -> rule4) OR ((((triple9) -> rule3) triple10) -> rule5) OR ((((triple9) -> rule3) triple9) -> rule4))] Gary is red.[(((triple14) -> rule2) OR ((((triple13 triple15) -> rule5)) -> rule2))] @2: Bob is red.[(((((triple1 triple2) -> rule5)) -> rule2))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
((triple6) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple6
((((triple5) -> (rule3 % int2)) triple5) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple8
((triple9) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple9
((((triple8 triple10) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Gary is blue.
("Gary" "is" "blue" "+")
triple11
Gary is furry.
("Gary" "is" "furry" "+")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
((((triple14) -> (rule2 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple14
((triple13 triple15) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple15
Bob is round.
("Bob" "is" "round" "+")
((triple1 triple2) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple5) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((triple8 triple10) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple8 triple9) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple9) -> (rule3 % int2)) triple10) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((triple9) -> (rule3 % int2)) triple9) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((triple14) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple13 triple15) -> (rule5 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((triple1 triple2) -> (rule5 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2