Bob is quiet. Bob is rough. Bob is smart. Dave is not green. Dave is not quiet. Dave is rough. Dave is smart. Gary is not blue. Gary is green. Harry is blue. Harry is nice. Harry is smart. If someone is green and not smart then they are blue. Smart people are blue. Blue people are nice. If someone is blue and not smart then they are rough. If someone is green and blue then they are rough. Quiet, smart people are rough. If someone is smart and green then they are cold. Nice people are not cold.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is green.
("Gary" "is" "green" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is green and not smart then they are blue.
((("someone" "is" "green" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "blue" "+"))
Smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is blue and not smart then they are rough.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "rough" "+"))
If someone is green and blue then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Quiet, smart people are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If someone is smart and green then they are cold.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Nice people are not cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "-"))
Gary is not blue.
True
1
proof
[(triple8)]
("Gary" "is" "blue" "-")
triple8
Dave is green.
False
1
inv-proof
[(triple4)]
("Dave" "is" "green" "+")
triple4
Dave is blue.
True
2
proof
[(((triple7) -> rule2))]
("Dave" "is" "blue" "+")
((triple7) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple7) -> rule2))]
("Dave" "is" "blue" "-")
((triple7) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
True
3
proof
[(((((triple7) -> rule2)) -> rule3))]
("Dave" "is" "nice" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not nice.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule3))]
("Dave" "is" "nice" "-")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "cold" "+")
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "rough" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Bob is quiet.[(triple1)] Bob is rough.[(triple2 OR ((triple1 triple3) -> rule6))] Bob is smart.[(triple3)] Dave is not green.[(triple4)] Dave is not quiet.[(triple5)] Dave is rough.[(triple6)] Dave is smart.[(triple7)] Gary is green.[(triple9)] Gary is not blue.[(triple8)] Harry is blue.[(triple10 OR ((triple12) -> rule2))] Harry is nice.[(triple11 OR ((triple10) -> rule3) OR ((((triple12) -> rule2)) -> rule3))] Harry is smart.[(triple12)] @1: Bob is blue.[(((triple3) -> rule2))] Dave is blue.[(((triple7) -> rule2))] Harry is not cold.[(((triple11) -> rule8) OR ((((triple10) -> rule3)) -> rule8) OR ((((((triple12) -> rule2)) -> rule3)) -> rule8))] @2: Bob is nice.[(((((triple3) -> rule2)) -> rule3))] Dave is nice.[(((((triple7) -> rule2)) -> rule3))] @3: Bob is not cold.[(((((((triple3) -> rule2)) -> rule3)) -> rule8))] Dave is not cold.[(((((((triple7) -> rule2)) -> rule3)) -> rule8))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
((triple1 triple3) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Dave is not green.
("Dave" "is" "green" "-")
triple4
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple5
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
triple9
Gary is not blue.
("Gary" "is" "blue" "-")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple10
((triple12) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple11
((triple10) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple12) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Bob is blue.
("Bob" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple7) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
((triple11) -> (rule8 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
((((triple10) -> (rule3 % int2))) -> (rule8 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((((triple12) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Bob is not cold.
("Bob" "is" "cold" "-")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Dave is not cold.
("Dave" "is" "cold" "-")
((((((triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3