Bob is blue. Bob is nice. Bob is red. Bob is rough. Bob is round. Bob is smart. Charlie is not big. Charlie is blue. Charlie is not nice. Charlie is red. Charlie is rough. Charlie is not round. Gary is blue. Gary is nice. Gary is rough. Gary is not smart. Nice things are blue. If Bob is big and Bob is not nice then Bob is smart. All big, rough things are red. All nice things are big. If something is rough and not blue then it is big. Rough, smart things are round. If something is nice and not big then it is round. If something is smart and not rough then it is round.
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 round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
Nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If Bob is big and Bob is not nice then Bob is smart.
((("Bob" "is" "big" "+") ("Bob" "is" "nice" "~")) -> ("Bob" "is" "smart" "+"))
All big, rough things are red.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is rough and not blue then it is big.
((("something" "is" "rough" "+") ("something" "is" "blue" "~")) -> ("something" "is" "big" "+"))
Rough, smart things are round.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If something is nice and not big then it is round.
((("something" "is" "nice" "+") ("something" "is" "big" "~")) -> ("something" "is" "round" "+"))
If something is smart and not rough then it is round.
((("something" "is" "smart" "+") ("something" "is" "rough" "~")) -> ("something" "is" "round" "+"))
Bob is red.
True
1
proof
[(triple3 OR ((((triple2) -> rule4) triple4) -> rule3))]
("Bob" "is" "red" "+")
triple3
((((triple2) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not blue.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule1))]
("Bob" "is" "blue" "-")
triple1
((triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
True
2
proof
[(((triple2) -> rule4))]
("Bob" "is" "big" "+")
((triple2) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple14) -> rule4))]
("Gary" "is" "big" "-")
((triple14) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
True
4
proof
[(((((triple14) -> rule4) triple15) -> rule3))]
("Gary" "is" "red" "+")
((((triple14) -> (rule4 % int2)) triple15) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not red.
False
4
inv-proof
[(((((triple14) -> rule4) triple15) -> rule3))]
("Gary" "is" "red" "-")
((((triple14) -> (rule4 % int2)) triple15) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "round" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Bob is blue.[(triple1 OR ((triple2) -> rule1))] Bob is nice.[(triple2)] Bob is red.[(triple3 OR ((((triple2) -> rule4) triple4) -> rule3))] Bob is rough.[(triple4)] Bob is round.[(triple5 OR ((triple4 triple6) -> rule6))] Bob is smart.[(triple6)] Charlie is blue.[(triple8)] Charlie is not big.[(triple7)] Charlie is not nice.[(triple9)] Charlie is not round.[(triple12)] Charlie is red.[(triple10)] Charlie is rough.[(triple11)] Gary is blue.[(triple13 OR ((triple14) -> rule1))] Gary is nice.[(triple14)] Gary is not smart.[(triple16)] Gary is rough.[(triple15)] @1: Bob is big.[(((triple2) -> rule4))] Gary is big.[(((triple14) -> rule4))] @2: Gary is red.[(((((triple14) -> rule4) triple15) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
((((triple2) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
((triple4 triple6) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is not big.
("Charlie" "is" "big" "-")
triple7
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple9
Charlie is not round.
("Charlie" "is" "round" "-")
triple12
Charlie is red.
("Charlie" "is" "red" "+")
triple10
Charlie is rough.
("Charlie" "is" "rough" "+")
triple11
Gary is blue.
("Gary" "is" "blue" "+")
triple13
((triple14) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple14
Gary is not smart.
("Gary" "is" "smart" "-")
triple16
Gary is rough.
("Gary" "is" "rough" "+")
triple15
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple14) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((((triple14) -> (rule4 % int2)) triple15) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2