Bob is not blue. Bob is not nice. Bob is round. Dave is big. Dave is cold. Dave is kind. Fiona is big. Fiona is not blue. Fiona is cold. Fiona is not kind. Fiona is nice. Fiona is quiet. Blue things are not round. Nice, kind things are blue. All big things are nice.
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is round.
("Bob" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is not blue.
("Fiona" "is" "blue" "-")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is not kind.
("Fiona" "is" "kind" "-")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Blue things are not round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "-"))
Nice, kind things are blue.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Fiona is not kind.
True
1
proof
[(triple10)]
("Fiona" "is" "kind" "-")
triple10
Bob is blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Dave is nice.
True
2
proof
[(((triple4) -> rule3))]
("Dave" "is" "nice" "+")
((triple4) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple4) -> rule3))]
("Dave" "is" "nice" "-")
((triple4) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
True
4
proof
[(((((triple4) -> rule3) triple6) -> rule2))]
("Dave" "is" "blue" "+")
((((triple4) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not blue.
False
4
inv-proof
[(((((triple4) -> rule3) triple6) -> rule2))]
("Dave" "is" "blue" "-")
((((triple4) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not round.
True
5
proof
[(((((((triple4) -> rule3) triple6) -> rule2)) -> rule1))]
("Dave" "is" "round" "-")
((((((triple4) -> (rule3 % int3)) triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is round.
False
5
inv-proof
[(((((((triple4) -> rule3) triple6) -> rule2)) -> rule1))]
("Dave" "is" "round" "+")
((((((triple4) -> (rule3 % int3)) triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is not blue.[(triple1)] Bob is not nice.[(triple2)] Bob is round.[(triple3)] Dave is big.[(triple4)] Dave is cold.[(triple5)] Dave is kind.[(triple6)] Fiona is big.[(triple7)] Fiona is cold.[(triple9)] Fiona is nice.[(triple11 OR ((triple7) -> rule3))] Fiona is not blue.[(triple8)] Fiona is not kind.[(triple10)] Fiona is quiet.[(triple12)] @1: Dave is nice.[(((triple4) -> rule3))] @2: Dave is blue.[(((((triple4) -> rule3) triple6) -> rule2))] @3: Dave is not round.[(((((((triple4) -> rule3) triple6) -> rule2)) -> rule1))]
Bob is not blue.
("Bob" "is" "blue" "-")
triple1
Bob is not nice.
("Bob" "is" "nice" "-")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Fiona is big.
("Fiona" "is" "big" "+")
triple7
Fiona is cold.
("Fiona" "is" "cold" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple11
((triple7) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not blue.
("Fiona" "is" "blue" "-")
triple8
Fiona is not kind.
("Fiona" "is" "kind" "-")
triple10
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple12
Dave is nice.
("Dave" "is" "nice" "+")
((triple4) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple4) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not round.
("Dave" "is" "round" "-")
((((((triple4) -> (rule3 % int3)) triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3