Charlie is big. Charlie is kind. Charlie is young. Dave is kind. Dave is red. Fiona is furry. Fiona is kind. Fiona is young. Gary is blue. Gary is kind. Gary is round. Gary is young. All young, blue things are kind. Blue, young things are red. If something is kind then it is red.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
All young, blue things are kind.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Blue, young things are red.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is kind then it is red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Dave is kind.
True
1
proof
[(triple4)]
("Dave" "is" "kind" "+")
triple4
Fiona is not young.
False
1
inv-proof
[(triple8)]
("Fiona" "is" "young" "-")
triple8
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Charlie is big.[(triple1)] Charlie is kind.[(triple2)] Charlie is young.[(triple3)] Dave is kind.[(triple4)] Dave is red.[(triple5 OR ((triple4) -> rule3))] Fiona is furry.[(triple6)] Fiona is kind.[(triple7)] Fiona is young.[(triple8)] Gary is blue.[(triple9)] Gary is kind.[(triple10 OR ((triple12 triple9) -> rule1))] Gary is round.[(triple11)] Gary is young.[(triple12)] @1: Charlie is red.[(((triple2) -> rule3))] Fiona is red.[(((triple7) -> rule3))] Gary is red.[(((triple10) -> rule3) OR ((triple9 triple12) -> rule2) OR ((((triple12 triple9) -> rule1)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
((triple4) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple6
Fiona is kind.
("Fiona" "is" "kind" "+")
triple7
Fiona is young.
("Fiona" "is" "young" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
((triple12 triple9) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
Charlie is red.
("Charlie" "is" "red" "+")
((triple2) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple7) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple10) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple9 triple12) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple12 triple9) -> (rule1 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2