Bob is nice. Bob is quiet. Bob is red. Bob is smart. Fiona is cold. Fiona is furry. Fiona is nice. Fiona is quiet. Fiona is red. Fiona is round. Fiona is not smart. Harry is not cold. Harry is nice. Harry is quiet. Harry is red. Harry is round. If something is red then it is round. Cold things are round. If Bob is not quiet then Bob is round. If Bob is furry then Bob is round. If Bob is nice and Bob is not quiet then Bob is red. If Bob is round then Bob is cold.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is not smart.
("Fiona" "is" "smart" "-")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is red then it is round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If Bob is not quiet then Bob is round.
((("Bob" "is" "quiet" "~")) -> ("Bob" "is" "round" "+"))
If Bob is furry then Bob is round.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "round" "+"))
If Bob is nice and Bob is not quiet then Bob is red.
((("Bob" "is" "nice" "+") ("Bob" "is" "quiet" "~")) -> ("Bob" "is" "red" "+"))
If Bob is round then Bob is cold.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "cold" "+"))
Harry is red.
True
1
proof
[(triple15)]
("Harry" "is" "red" "+")
triple15
Bob is not red.
False
1
inv-proof
[(triple3)]
("Bob" "is" "red" "-")
triple3
Bob is round.
True
2
proof
[(((triple3) -> rule1))]
("Bob" "is" "round" "+")
((triple3) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple3) -> rule1))]
("Bob" "is" "round" "-")
((triple3) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is cold.
True
3
proof
[(((((triple3) -> rule1)) -> rule6))]
("Bob" "is" "cold" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not cold.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule6))]
("Bob" "is" "cold" "-")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is nice.[(triple1)] Bob is quiet.[(triple2)] Bob is red.[(triple3)] Bob is smart.[(triple4)] Fiona is cold.[(triple5)] Fiona is furry.[(triple6)] Fiona is nice.[(triple7)] Fiona is not smart.[(triple11)] Fiona is quiet.[(triple8)] Fiona is red.[(triple9)] Fiona is round.[(triple10 OR ((triple5) -> rule2) OR ((triple9) -> rule1))] Harry is nice.[(triple13)] Harry is not cold.[(triple12)] Harry is quiet.[(triple14)] Harry is red.[(triple15)] Harry is round.[(triple16 OR ((triple15) -> rule1))] @1: Bob is round.[(((triple3) -> rule1))] @2: Bob is cold.[(((((triple3) -> rule1)) -> rule6))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Fiona is cold.
("Fiona" "is" "cold" "+")
triple5
Fiona is furry.
("Fiona" "is" "furry" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
Fiona is not smart.
("Fiona" "is" "smart" "-")
triple11
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple8
Fiona is red.
("Fiona" "is" "red" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
((triple5) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple9) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple13
Harry is not cold.
("Harry" "is" "cold" "-")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is red.
("Harry" "is" "red" "+")
triple15
Harry is round.
("Harry" "is" "round" "+")
triple16
((triple15) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple3) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2