Bob is cold. Bob is nice. Bob is smart. Dave is green. Dave is nice. Dave is round. Dave is smart. Dave is white. Fiona is cold. Fiona is green. Fiona is nice. Fiona is quiet. Fiona is round. Fiona is smart. Fiona is white. If something is quiet then it is cold. If Fiona is cold then Fiona is nice. All green, white things are quiet.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If something is quiet then it is cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If Fiona is cold then Fiona is nice.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "nice" "+"))
All green, white things are quiet.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Fiona is smart.
True
1
proof
[(triple14)]
("Fiona" "is" "smart" "+")
triple14
Dave is not nice.
False
1
inv-proof
[(triple5)]
("Dave" "is" "nice" "-")
triple5
Dave is quiet.
True
3
proof
[(((triple4 triple8) -> rule3))]
("Dave" "is" "quiet" "+")
((triple4 triple8) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
3
inv-proof
[(((triple4 triple8) -> rule3))]
("Dave" "is" "quiet" "-")
((triple4 triple8) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
True
4
proof
[(((((triple4 triple8) -> rule3)) -> rule1))]
("Dave" "is" "cold" "+")
((((triple4 triple8) -> (rule3 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not cold.
False
4
inv-proof
[(((((triple4 triple8) -> rule3)) -> rule1))]
("Dave" "is" "cold" "-")
((((triple4 triple8) -> (rule3 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is cold.[(triple1)] Bob is nice.[(triple2)] Bob is smart.[(triple3)] Dave is green.[(triple4)] Dave is nice.[(triple5)] Dave is round.[(triple6)] Dave is smart.[(triple7)] Dave is white.[(triple8)] Fiona is cold.[(triple9 OR ((triple12) -> rule1) OR ((((triple10 triple15) -> rule3)) -> rule1))] Fiona is green.[(triple10)] Fiona is nice.[(triple11 OR ((triple9) -> rule2) OR ((((triple12) -> rule1)) -> rule2) OR ((((((triple10 triple15) -> rule3)) -> rule1)) -> rule2))] Fiona is quiet.[(triple12 OR ((triple10 triple15) -> rule3))] Fiona is round.[(triple13)] Fiona is smart.[(triple14)] Fiona is white.[(triple15)] @1: Dave is quiet.[(((triple4 triple8) -> rule3))] @2: Dave is cold.[(((((triple4 triple8) -> rule3)) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
triple8
Fiona is cold.
("Fiona" "is" "cold" "+")
triple9
((triple12) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple10 triple15) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
triple10
Fiona is nice.
("Fiona" "is" "nice" "+")
triple11
((triple9) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((((triple10 triple15) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple12
((triple10 triple15) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple13
Fiona is smart.
("Fiona" "is" "smart" "+")
triple14
Fiona is white.
("Fiona" "is" "white" "+")
triple15
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple4 triple8) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple4 triple8) -> (rule3 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2