Bob is quiet. Bob is red. Charlie is not cold. Charlie is nice. Charlie is not quiet. Charlie is red. Charlie is rough. Charlie is smart. Erin is red. Erin is rough. Erin is smart. Harry is cold. Harry is green. Harry is not red. Harry is rough. All green people are nice. All nice, green people are quiet. All quiet people are green.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is rough.
("Harry" "is" "rough" "+")
All green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
All nice, green people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Charlie is not quiet.
True
1
proof
[(triple5)]
("Charlie" "is" "quiet" "-")
triple5
Harry is not cold.
False
1
inv-proof
[(triple12)]
("Harry" "is" "cold" "-")
triple12
Bob is green.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "green" "+")
((triple1) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "green" "-")
((triple1) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Harry is quiet.
True
4
proof
[(((((triple13) -> rule1) triple13) -> rule2))]
("Harry" "is" "quiet" "+")
((((triple13) -> (rule1 % int2)) triple13) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "green" "-")
Erin is green.
Unknown
rconc
[@2: Erin is green.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Erin" "is" "green" "+")
Erin is not nice.
Unknown
inv-rconc
[@3: Erin is nice.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- FAIL)]]
("Erin" "is" "nice" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is quiet.[(triple1)] Bob is red.[(triple2)] Charlie is nice.[(triple4)] Charlie is not cold.[(triple3)] Charlie is not quiet.[(triple5)] Charlie is red.[(triple6)] Charlie is rough.[(triple7)] Charlie is smart.[(triple8)] Erin is red.[(triple9)] Erin is rough.[(triple10)] Erin is smart.[(triple11)] Harry is cold.[(triple12)] Harry is green.[(triple13)] Harry is not red.[(triple14)] Harry is rough.[(triple15)] @1: Bob is green.[(((triple1) -> rule3))] Harry is nice.[(((triple13) -> rule1))] @2: Bob is nice.[(((((triple1) -> rule3)) -> rule1))] Harry is quiet.[(((((triple13) -> rule1) triple13) -> rule2))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple3
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
Erin is red.
("Erin" "is" "red" "+")
triple9
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple11
Harry is cold.
("Harry" "is" "cold" "+")
triple12
Harry is green.
("Harry" "is" "green" "+")
triple13
Harry is not red.
("Harry" "is" "red" "-")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple13) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple13) -> (rule1 % int2)) triple13) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2