Bob is big. Bob is not blue. Bob is furry. Bob is red. Bob is smart. Charlie is big. Charlie is furry. Charlie is red. Charlie is smart. Dave is not big. Dave is furry. Dave is not quiet. Dave is not smart. Fiona is blue. Fiona is not furry. If something is furry and not quiet then it is cold. If something is cold and not big then it is blue.
Bob is big.
("Bob" "is" "big" "+")
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is not smart.
("Dave" "is" "smart" "-")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is not furry.
("Fiona" "is" "furry" "-")
If something is furry and not quiet then it is cold.
((("something" "is" "furry" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "cold" "+"))
If something is cold and not big then it is blue.
((("something" "is" "cold" "+") ("something" "is" "big" "~")) -> ("something" "is" "blue" "+"))
Bob is smart.
True
1
proof
[(triple5)]
("Bob" "is" "smart" "+")
triple5
Bob is not furry.
False
1
inv-proof
[(triple3)]
("Bob" "is" "furry" "-")
triple3
Dave is cold.
True
3
proof
[(((triple11 triple12) -> rule1))]
("Dave" "is" "cold" "+")
((triple11 triple12) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
3
inv-proof
[(((triple11 triple12) -> rule1))]
("Dave" "is" "cold" "-")
((triple11 triple12) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
True
5
proof
[(((((triple11 triple12) -> rule1) triple10) -> rule2))]
("Dave" "is" "blue" "+")
((((triple11 triple12) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not blue.
False
5
inv-proof
[(((((triple11 triple12) -> rule1) triple10) -> rule2))]
("Dave" "is" "blue" "-")
((((triple11 triple12) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "cold" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "blue" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is big.[(triple1)] Bob is furry.[(triple3)] Bob is not blue.[(triple2)] Bob is red.[(triple4)] Bob is smart.[(triple5)] Charlie is big.[(triple6)] Charlie is furry.[(triple7)] Charlie is red.[(triple8)] Charlie is smart.[(triple9)] Dave is furry.[(triple11)] Dave is not big.[(triple10)] Dave is not quiet.[(triple12)] Dave is not smart.[(triple13)] Fiona is blue.[(triple14)] Fiona is not furry.[(triple15)] @1: Dave is cold.[(((triple11 triple12) -> rule1))] @2: Dave is blue.[(((((triple11 triple12) -> rule1) triple10) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is not blue.
("Bob" "is" "blue" "-")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
Charlie is red.
("Charlie" "is" "red" "+")
triple8
Charlie is smart.
("Charlie" "is" "smart" "+")
triple9
Dave is furry.
("Dave" "is" "furry" "+")
triple11
Dave is not big.
("Dave" "is" "big" "-")
triple10
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple12
Dave is not smart.
("Dave" "is" "smart" "-")
triple13
Fiona is blue.
("Fiona" "is" "blue" "+")
triple14
Fiona is not furry.
("Fiona" "is" "furry" "-")
triple15
Dave is cold.
("Dave" "is" "cold" "+")
((triple11 triple12) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple11 triple12) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2