Bob is blue. Bob is nice. Bob is red. Dave is big. Dave is green. Dave is not nice. Dave is smart. Dave is white. Fiona is big. Fiona is green. Fiona is red. Fiona is smart. All white, nice things are smart. Blue things are smart. All blue things are white. If Bob is not green and Bob is not big then Bob is smart. If Dave is smart and Dave is blue then Dave is not nice. If Dave is white then Dave is not nice. If Bob is smart and Bob is white then Bob is nice. All green things are blue.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
All white, nice things are smart.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
All blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
If Bob is not green and Bob is not big then Bob is smart.
((("Bob" "is" "green" "~") ("Bob" "is" "big" "~")) -> ("Bob" "is" "smart" "+"))
If Dave is smart and Dave is blue then Dave is not nice.
((("Dave" "is" "smart" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "nice" "-"))
If Dave is white then Dave is not nice.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "nice" "-"))
If Bob is smart and Bob is white then Bob is nice.
((("Bob" "is" "smart" "+") ("Bob" "is" "white" "+")) -> ("Bob" "is" "nice" "+"))
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Dave is big.
True
1
proof
[(triple4)]
("Dave" "is" "big" "+")
triple4
Bob is not red.
False
1
inv-proof
[(triple3)]
("Bob" "is" "red" "-")
triple3
Bob is white.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "white" "+")
((triple1) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple5) -> rule8))]
("Dave" "is" "blue" "-")
((triple5) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Fiona is white.
True
3
proof
[(((((triple10) -> rule8)) -> rule3))]
("Fiona" "is" "white" "+")
((((triple10) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is not white.
False
3
inv-proof
[(((((triple10) -> rule8)) -> rule3))]
("Fiona" "is" "white" "-")
((((triple10) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is blue.[(triple1)] Bob is nice.[(triple2 OR ((((triple1) -> rule2) ((triple1) -> rule3)) -> rule7))] Bob is red.[(triple3)] Dave is big.[(triple4)] Dave is green.[(triple5)] Dave is not nice.[(triple6 OR ((triple8) -> rule6) OR ((triple7 ((triple5) -> rule8)) -> rule5) OR ((((((triple5) -> rule8)) -> rule3)) -> rule6) OR ((((((triple5) -> rule8)) -> rule2) ((triple5) -> rule8)) -> rule5))] Dave is smart.[(triple7 OR ((((triple5) -> rule8)) -> rule2))] Dave is white.[(triple8 OR ((((triple5) -> rule8)) -> rule3))] Fiona is big.[(triple9)] Fiona is green.[(triple10)] Fiona is red.[(triple11)] Fiona is smart.[(triple12 OR ((((triple10) -> rule8)) -> rule2))] @1: Bob is smart.[(((triple1) -> rule2) OR ((((triple1) -> rule3) triple2) -> rule1))] Bob is white.[(((triple1) -> rule3))] Dave is blue.[(((triple5) -> rule8))] Fiona is blue.[(((triple10) -> rule8))] @2: Fiona is white.[(((((triple10) -> rule8)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
((((triple1) -> (rule2 % int3)) ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is not nice.
("Dave" "is" "nice" "-")
triple6
((triple8) -> (rule6 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
((triple7 ((triple5) -> (rule8 % int2))) -> (rule5 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((((triple5) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((((triple5) -> (rule8 % int3))) -> (rule2 % int2)) ((triple5) -> (rule8 % int3))) -> (rule5 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
triple7
((((triple5) -> (rule8 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple8
((((triple5) -> (rule8 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
triple9
Fiona is green.
("Fiona" "is" "green" "+")
triple10
Fiona is red.
("Fiona" "is" "red" "+")
triple11
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
((((triple10) -> (rule8 % int2))) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple1) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple5) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple10) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((((triple10) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2