Bob is not big. Bob is blue. Bob is quiet. Bob is red. Bob is rough. Charlie is big. Charlie is blue. Charlie is quiet. Charlie is not red. Charlie is not white. Charlie is young. Harry is big. Harry is quiet. Harry is not rough. Harry is white. Harry is not young. If someone is red and not white then they are big. Blue, white people are rough. Young, white people are not rough. Blue people are rough. All young people are not red. All rough, red people are blue. If Bob is red and Bob is not white then Bob is young. If someone is red and not blue then they are quiet.
Bob is not big.
("Bob" "is" "big" "-")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Charlie is not white.
("Charlie" "is" "white" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is white.
("Harry" "is" "white" "+")
Harry is not young.
("Harry" "is" "young" "-")
If someone is red and not white then they are big.
((("someone" "is" "red" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "big" "+"))
Blue, white people are rough.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
Young, white people are not rough.
((("someone" "is" "young" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "rough" "-"))
Blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
All young people are not red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "-"))
All rough, red people are blue.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If Bob is red and Bob is not white then Bob is young.
((("Bob" "is" "red" "+") ("Bob" "is" "white" "~")) -> ("Bob" "is" "young" "+"))
If someone is red and not blue then they are quiet.
((("someone" "is" "red" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "quiet" "+"))
Charlie is quiet.
True
1
proof
[(triple8)]
("Charlie" "is" "quiet" "+")
triple8
Charlie is red.
False
1
inv-proof
[(triple9 OR ((triple11) -> rule5))]
("Charlie" "is" "red" "+")
triple9
((triple11) -> (rule5 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is rough.
True
2
proof
[(((triple7) -> rule4))]
("Charlie" "is" "rough" "+")
((triple7) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple7) -> rule4))]
("Charlie" "is" "rough" "-")
((triple7) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "young" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "blue" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is blue.[(triple2 OR ((triple5 triple4) -> rule6))] Bob is not big.[(triple1)] Bob is quiet.[(triple3)] Bob is red.[(triple4)] Bob is rough.[(triple5 OR ((triple2) -> rule4))] Charlie is big.[(triple6)] Charlie is blue.[(triple7)] Charlie is not red.[(triple9 OR ((triple11) -> rule5))] Charlie is not white.[(triple10)] Charlie is quiet.[(triple8)] Charlie is young.[(triple11)] Harry is big.[(triple12)] Harry is not rough.[(triple14)] Harry is not young.[(triple16)] Harry is quiet.[(triple13)] Harry is white.[(triple15)] @1: Charlie is rough.[(((triple7) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple5 triple4) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple2) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is blue.
("Charlie" "is" "blue" "+")
triple7
Charlie is not red.
("Charlie" "is" "red" "-")
triple9
((triple11) -> (rule5 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is not white.
("Charlie" "is" "white" "-")
triple10
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple8
Charlie is young.
("Charlie" "is" "young" "+")
triple11
Harry is big.
("Harry" "is" "big" "+")
triple12
Harry is not rough.
("Harry" "is" "rough" "-")
triple14
Harry is not young.
("Harry" "is" "young" "-")
triple16
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is white.
("Harry" "is" "white" "+")
triple15
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple7) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1